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