let K be Field; :: thesis: for T being K -monomorphic comRing
for f being Monomorphism of K,T
for a, b being Element of (embField f)
for a1, b1 being Element of T st not a in [#] K & not b in [#] K & the addF of T . (a,b) in rng f & a1 = a & b1 = b holds
( a + b = (f ") . (a1 + b1) & b + a = (f ") . (b1 + a1) & a + b in [#] K & b + a in [#] K )
let T be K -monomorphic comRing; :: thesis: for f being Monomorphism of K,T
for a, b being Element of (embField f)
for a1, b1 being Element of T st not a in [#] K & not b in [#] K & the addF of T . (a,b) in rng f & a1 = a & b1 = b holds
( a + b = (f ") . (a1 + b1) & b + a = (f ") . (b1 + a1) & a + b in [#] K & b + a in [#] K )
let f be Monomorphism of K,T; :: thesis: for a, b being Element of (embField f)
for a1, b1 being Element of T st not a in [#] K & not b in [#] K & the addF of T . (a,b) in rng f & a1 = a & b1 = b holds
( a + b = (f ") . (a1 + b1) & b + a = (f ") . (b1 + a1) & a + b in [#] K & b + a in [#] K )
let a, b be Element of (embField f); :: thesis: for a1, b1 being Element of T st not a in [#] K & not b in [#] K & the addF of T . (a,b) in rng f & a1 = a & b1 = b holds
( a + b = (f ") . (a1 + b1) & b + a = (f ") . (b1 + a1) & a + b in [#] K & b + a in [#] K )
let a1, b1 be Element of T; :: thesis: ( not a in [#] K & not b in [#] K & the addF of T . (a,b) in rng f & a1 = a & b1 = b implies ( a + b = (f ") . (a1 + b1) & b + a = (f ") . (b1 + a1) & a + b in [#] K & b + a in [#] K ) )
assume AS: ( not a in [#] K & not b in [#] K & the addF of T . (a,b) in rng f & a1 = a & b1 = b ) ; :: thesis: ( a + b = (f ") . (a1 + b1) & b + a = (f ") . (b1 + a1) & a + b in [#] K & b + a in [#] K )
reconsider ac = a, bc = b as Element of carr f by defemb;
thus D: a + b = (addemb f) . (a,b) by defemb
.= addemb (f,ac,bc) by defadd
.= (f ") . (a1 + b1) by AS, defaddf ; :: thesis: ( b + a = (f ") . (b1 + a1) & a + b in [#] K & b + a in [#] K )
C: the addF of T . (a1,b1) = a1 + b1
.= b1 + a1
.= the addF of T . (b1,a1) ;
thus E: b + a = (addemb f) . (b,a) by defemb
.= addemb (f,bc,ac) by defadd
.= (f ") . (b1 + a1) by C, AS, defaddf ; :: thesis: ( a + b in [#] K & b + a in [#] K )
a1 + b1 in dom (f ") by AS, FUNCT_1:33;
then F: (f ") . (a1 + b1) in rng (f ") by FUNCT_1:def 3;
hence a + b in [#] K by D; :: thesis: b + a in [#] K
thus b + a in [#] K by E, F; :: thesis: verum