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 K,T are_disjoint & not a in [#] K & not b in [#] K & not the multF of T . (a,b) in rng f & a1 = a & b1 = b holds
( a * b = a1 * b1 & b * a = b1 * 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
for a, b being Element of (embField f)
for a1, b1 being Element of T st K,T are_disjoint & not a in [#] K & not b in [#] K & not the multF of T . (a,b) in rng f & a1 = a & b1 = b holds
( a * b = a1 * b1 & b * a = b1 * a1 & not a * b in [#] K & not 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 K,T are_disjoint & not a in [#] K & not b in [#] K & not the multF of T . (a,b) in rng f & a1 = a & b1 = b holds
( a * b = a1 * b1 & b * a = b1 * a1 & not a * b in [#] K & not b * a in [#] K )
let a, b be Element of (embField f); :: thesis: for a1, b1 being Element of T st K,T are_disjoint & not a in [#] K & not b in [#] K & not the multF of T . (a,b) in rng f & a1 = a & b1 = b holds
( a * b = a1 * b1 & b * a = b1 * a1 & not a * b in [#] K & not b * a in [#] K )
let a1, b1 be Element of T; :: thesis: ( K,T are_disjoint & not a in [#] K & not b in [#] K & not the multF of T . (a,b) in rng f & a1 = a & b1 = b implies ( a * b = a1 * b1 & b * a = b1 * a1 & not a * b in [#] K & not b * a in [#] K ) )
assume AS: ( K,T are_disjoint & not a in [#] K & not b in [#] K & not the multF of T . (a,b) in rng f & a1 = a & b1 = b ) ; :: thesis: ( a * b = a1 * b1 & b * a = b1 * a1 & not a * b in [#] K & not b * a in [#] K )
then B1: ( a <> 0. K & b <> 0. K ) ;
reconsider ac = a, bc = b as Element of carr f by defemb;
thus D1: a * b = (multemb f) . (a,b) by defemb
.= multemb (f,ac,bc) by defmult
.= a1 * b1 by B1, AS, defmultf ; :: thesis: ( b * a = b1 * a1 & not a * b in [#] K & not b * a in [#] K )
C1: the multF of T . (a1,b1) = a1 * b1
.= b1 * a1 by GROUP_1:def 12
.= the multF of T . (b1,a1) ;
thus b * a = (multemb f) . (b,a) by defemb
.= multemb (f,bc,ac) by defmult
.= b1 * a1 by B1, C1, AS, defmultf ; :: thesis: ( not a * b in [#] K & not b * a in [#] K )
hence ( not a * b in [#] K & not b * a in [#] K ) by D1, AS, XBOOLE_0:def 4; :: thesis: verum