let K be Field; 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 multF 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; 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 multF 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; 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 multF 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); for a1, b1 being Element of T st not a in [#] K & not b in [#] K & the multF 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; ( not a in [#] K & not b in [#] K & the multF 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 multF of T . (a,b) in rng f & a1 = a & b1 = b )
; ( 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 D1: a * b =
(multemb f) . (a,b)
by defemb
.=
multemb (f,ac,bc)
by defmult
.=
(f ") . (a1 * b1)
by AS, defmultf
; ( b * a = (f ") . (b1 * a1) & a * b in [#] K & 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 E1: b * a =
(multemb f) . (b,a)
by defemb
.=
multemb (f,bc,ac)
by defmult
.=
(f ") . (b1 * a1)
by C1, AS, defmultf
; ( a * b in [#] K & b * a in [#] K )
a1 * b1 in dom (f ")
by AS, FUNCT_1:33;
then G1:
(f ") . (a1 * b1) in rng (f ")
by FUNCT_1:def 3;
hence
a * b in [#] K
by D1; b * a in [#] K
(f ") . (a1 * b1) in dom f
by G1, FUNCT_1:33;
then
(f ") . (b1 * a1) in dom f
by GROUP_1:def 12;
hence
b * a in [#] K
by E1; verum