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 K st a1 = a & b1 = b holds
( a + b = a1 + b1 & b + a = b1 + a1 )
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 K st a1 = a & b1 = b holds
( a + b = a1 + b1 & b + a = b1 + a1 )
let f be Monomorphism of K,T; :: thesis: for a, b being Element of (embField f)
for a1, b1 being Element of K st a1 = a & b1 = b holds
( a + b = a1 + b1 & b + a = b1 + a1 )
let a, b be Element of (embField f); :: thesis: for a1, b1 being Element of K st a1 = a & b1 = b holds
( a + b = a1 + b1 & b + a = b1 + a1 )
let a1, b1 be Element of K; :: thesis: ( a1 = a & b1 = b implies ( a + b = a1 + b1 & b + a = b1 + a1 ) )
assume A1: ( a1 = a & b1 = b ) ; :: thesis: ( a + b = a1 + b1 & b + a = b1 + a1 )
reconsider ac = a, bc = b as Element of carr f by defemb;
thus a + b = (addemb f) . (a,b) by defemb
.= addemb (f,ac,bc) by defadd
.= a1 + b1 by A1, defaddf ; :: thesis: b + a = b1 + a1
thus b + a = (addemb f) . (b,a) by defemb
.= addemb (f,bc,ac) by defadd
.= b1 + a1 by A1, defaddf ; :: thesis: verum