+axiom symmetric_a_mult: ∀K.∀A:f_algebra K. symmetric ? (a_mult ? ? A).
+
+
+definition tends_to : ∀F:ordered_field_ch0.∀f:nat→F.∀l:F.Prop.
+ alias symbol "leq" = "Ordered field le".
+ alias id "le" = "cic:/matita/nat/orders/le.ind#xpointer(1/1)".
+ apply
+ (λF:ordered_field_ch0.λf:nat → F.λl:F.
+ ∀n:nat.∃m:nat.∀j:nat. le m j →
+ l - (inv F (sum_field F (S n)) ?) ≤ f j ∧
+ f j ≤ l + (inv F (sum_field F (S n)) ?));
+ apply not_eq_sum_field_zero;
+ unfold;
+ auto new.
+qed.
+
+record is_integral (K) (A:f_algebra K) (I:Type_OF_f_algebra ? A→K) : Prop
+\def
+ { i_positive: ∀f:Type_OF_f_algebra ? A. le ? (lattice_OF_f_algebra ? A) 0 f → of_le K 0 (I f);
+ i_linear1: ∀f,g:Type_OF_f_algebra ? A. I (f + g) = I f + I g;
+ i_linear2: ∀f:A.∀k:K. I (emult ? A k f) = k*(I f)
+ }.
+
+(* Here we are avoiding a construction (the quotient space to define
+ f=g iff I(|f-g|)=0 *)
+record is_integration_f_algebra (K) (A:f_algebra K) (I:Type_OF_f_algebra ? A→K) : Prop
+\def
+ { ifa_integral: is_integral ? ? I;
+ ifa_limit1:
+ ∀f:A. tends_to ? (λn.I(meet ? A f ((sum_field K n)*(a_one ? ? A)))) (I f);
+ ifa_limit2:
+ ∀f:A.
+ tends_to ?
+ (λn.
+ I (meet ? A f
+ ((inv ? (sum_field K (S n))
+ (not_eq_sum_field_zero K (S n) (le_S_S O n (le_O_n n)))
+ ) * (a_one ? ? A)))) 0;
+ ifa_quotient_space1:
+ ∀f,g:A. f=g → I(absolute_value ? A (f - g)) = 0
+ }.
\ No newline at end of file