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 K st a1 = a & b1 = b holds
( a * b = a1 * b1 & b * a = b1 * a1 )
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 K st a1 = a & b1 = b holds
( a * b = a1 * b1 & b * a = b1 * a1 )
let f be 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 a, b be 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 a1, b1 be Element of K; ( a1 = a & b1 = b implies ( a * b = a1 * b1 & b * a = b1 * a1 ) )
assume B1:
( a1 = a & b1 = b )
; ( a * b = a1 * b1 & b * a = b1 * a1 )
reconsider ac = a, bc = b as Element of carr f by defemb;
thus a * b =
(multemb f) . (a,b)
by defemb
.=
multemb (f,ac,bc)
by defmult
.=
a1 * b1
by B1, defmultf
; b * a = b1 * a1
thus b * a =
(multemb f) . (b,a)
by defemb
.=
multemb (f,bc,ac)
by defmult
.=
b1 * a1
by B1, defmultf
; verum