let K be Field; :: thesis: for T being K -monomorphic comRing
for f being Monomorphism of K,T st K,T are_disjoint holds
for a, b being Element of (embField f) st a in [#] K & not b in [#] K holds
for a1, b1 being Element of carr f st a1 = a & b1 = b holds
( a + b = the addF of T . ((f . a1),b1) & b + a = the addF of T . (b1,(f . a1)) & not a + b in [#] K & not b + a in [#] K )
let T be K -monomorphic comRing; :: thesis: for f being Monomorphism of K,T st K,T are_disjoint holds
for a, b being Element of (embField f) st a in [#] K & not b in [#] K holds
for a1, b1 being Element of carr f st a1 = a & b1 = b holds
( a + b = the addF of T . ((f . a1),b1) & b + a = the addF of T . (b1,(f . a1)) & not a + b in [#] K & not b + a in [#] K )
let f be Monomorphism of K,T; :: thesis: ( K,T are_disjoint implies for a, b being Element of (embField f) st a in [#] K & not b in [#] K holds
for a1, b1 being Element of carr f st a1 = a & b1 = b holds
( a + b = the addF of T . ((f . a1),b1) & b + a = the addF of T . (b1,(f . a1)) & not a + b in [#] K & not b + a in [#] K ) )
assume A1: K,T are_disjoint ; :: thesis: for a, b being Element of (embField f) st a in [#] K & not b in [#] K holds
for a1, b1 being Element of carr f st a1 = a & b1 = b holds
( a + b = the addF of T . ((f . a1),b1) & b + a = the addF of T . (b1,(f . a1)) & not a + b in [#] K & not b + a in [#] K )
let a, b be Element of (embField f); :: thesis: ( a in [#] K & not b in [#] K implies for a1, b1 being Element of carr f st a1 = a & b1 = b holds
( a + b = the addF of T . ((f . a1),b1) & b + a = the addF of T . (b1,(f . a1)) & not a + b in [#] K & not b + a in [#] K ) )
assume A2: ( a in [#] K & not b in [#] K ) ; :: thesis: for a1, b1 being Element of carr f st a1 = a & b1 = b holds
( a + b = the addF of T . ((f . a1),b1) & b + a = the addF of T . (b1,(f . a1)) & not a + b in [#] K & not b + a in [#] K )
let a1, b1 be Element of carr f; :: thesis: ( a1 = a & b1 = b implies ( a + b = the addF of T . ((f . a1),b1) & b + a = the addF of T . (b1,(f . a1)) & not a + b in [#] K & not b + a in [#] K ) )
assume A3: ( a1 = a & b1 = b ) ; :: thesis: ( a + b = the addF of T . ((f . a1),b1) & b + a = the addF of T . (b1,(f . a1)) & not a + b in [#] K & not b + a in [#] K )
thus A4: a + b = (addemb f) . (a,b) by defemb
.= addemb (f,a1,b1) by defadd, A3
.= the addF of T . ((f . a1),b1) by A2, A3, defaddf ; :: thesis: ( b + a = the addF of T . (b1,(f . a1)) & not a + b in [#] K & not b + a in [#] K )
thus A5: b + a = (addemb f) . (b,a) by defemb
.= addemb (f,b1,a1) by defadd, A3
.= the addF of T . (b1,(f . a1)) by A3, A2, defaddf ; :: thesis: ( not a + b in [#] K & not b + a in [#] K )
the addF of T . ((f . a1),b1) in ([#] T) \ (rng f) by A2, A3, Lm3;
hence not a + b in [#] K by A1, A4, XBOOLE_0:def 4; :: thesis: not b + a in [#] K
the addF of T . (b1,(f . a1)) in ([#] T) \ (rng f) by A3, A2, Lm2;
hence not b + a in [#] K by A1, A5, XBOOLE_0:def 4; :: thesis: verum