(cic:/matita/didactic/deriv/fplus.con x y).
axiom i:R→F. (*mappatura R in F*)
coercion cic:/matita/didactic/deriv/i.con.
(cic:/matita/didactic/deriv/fplus.con x y).
axiom i:R→F. (*mappatura R in F*)
coercion cic:/matita/didactic/deriv/i.con.
-axiom fplus_commutative: ∀ f,g:F. f ⊕ g = g ⊕ f.
-axiom fplus_associative: ∀ f,g,h:F. f ⊕ (g ⊕ h) = (f ⊕ g) ⊕ h.
-axiom fplus_neutral: ∀f:F. (i R0) ⊕ f = f.
+axiom fplus_commutative: ∀ f,g:F. f + g = g + f.
+axiom fplus_associative: ∀ f,g,h:F. f + (g + h) = (f + g) + h.
+axiom fplus_neutral: ∀f:F. (i R0) + f = f.
axiom fmult_commutative: ∀ f,g:F. f · g = g · f.
axiom fmult_associative: ∀ f,g,h:F. f · (g · h) = (f · g) · h.
axiom fmult_neutral: ∀f:F. (i R1) · f = f.
axiom fmult_assorb: ∀f:F. (i R0) · f = (i R0).
axiom fmult_commutative: ∀ f,g:F. f · g = g · f.
axiom fmult_associative: ∀ f,g,h:F. f · (g · h) = (f · g) · h.
axiom fmult_neutral: ∀f:F. (i R1) · f = f.
axiom fmult_assorb: ∀f:F. (i R0) · f = (i R0).