thus embField f is commutative :: thesis: embField f is well-unital

proof

now :: thesis: for a, b being Element of (embField f) holds a * b = b * a

let a, b be Element of (embField f); :: thesis: b₁ * b₂ = b₂ * b₁
reconsider x = a, y = b as Element of carr f by defemb;

per cases ( ( x in [#] K & y in [#] K ) or a = 0. K or b = 0. K or ( x in [#] K & x <> 0. K & not y in [#] K ) or ( y in [#] K & y <> 0. K & not x in [#] K ) or ( not x in [#] K & not y in [#] K & the multF of T . (x,y) in rng f ) or ( not x in [#] K & not y in [#] K & not the multF of T . (x,y) in rng f ) ) ;

suppose ( x in [#] K & y in [#] K ) ; :: thesis: b₁ * b₂ = b₂ * b₁

then reconsider a1 = a, b1 = b as Element of K ;
thus a * b = a1 * b1 by Lm11
.= b1 * a1 by GROUP_1:def 12
.= b * a by Lm11 ; :: thesis: verum

end;

suppose A: ( a = 0. K or b = 0. K ) ; :: thesis: b₁ * b₂ = b₂ * b₁

per cases ( a = 0. K or b = 0. K ) by A;

suppose A1: a = 0. K ; :: thesis: b₁ * b₂ = b₂ * b₁

thus a * b = (multemb f) . (x,y) by defemb
.= multemb (f,x,y) by defmult
.= 0. K by A1, defmultf
.= multemb (f,y,x) by A1, defmultf
.= (multemb f) . (y,x) by defmult
.= b * a by defemb ; :: thesis: verum

end;

suppose A1: b = 0. K ; :: thesis: b₁ * b₂ = b₂ * b₁

thus a * b = (multemb f) . (x,y) by defemb
.= multemb (f,x,y) by defmult
.= 0. K by A1, defmultf
.= multemb (f,y,x) by A1, defmultf
.= (multemb f) . (y,x) by defmult
.= b * a by defemb ; :: thesis: verum

end;

end;

end;

suppose A: ( x in [#] K & x <> 0. K & not y in [#] K ) ; :: thesis: b₁ * b₂ = b₂ * b₁

then reconsider a1 = a as Element of K ;
reconsider b1 = b as Element of T by A, Lm1;
reconsider fa = f . a1 as Element of T ;
thus a * b = (multemb f) . (x,y) by defemb
.= multemb (f,x,y) by defmult
.= fa * b1 by A, defmultf
.= b1 * fa by GROUP_1:def 12
.= multemb (f,y,x) by A, defmultf
.= (multemb f) . (y,x) by defmult
.= b * a by defemb ; :: thesis: verum

end;

suppose A: ( y in [#] K & y <> 0. K & not x in [#] K ) ; :: thesis: b₁ * b₂ = b₂ * b₁

then reconsider b1 = b as Element of K ;
reconsider a1 = a as Element of T by A, Lm1;
reconsider fb = f . b1 as Element of T ;
thus a * b = (multemb f) . (x,y) by defemb
.= multemb (f,x,y) by defmult
.= a1 * fb by A, defmultf
.= fb * a1 by GROUP_1:def 12
.= multemb (f,y,x) by A, defmultf
.= (multemb f) . (y,x) by defmult
.= b * a by defemb ; :: thesis: verum

end;

suppose A: ( not x in [#] K & not y in [#] K & the multF of T . (x,y) in rng f ) ; :: thesis: b₁ * b₂ = b₂ * b₁

then reconsider a1 = a, b1 = b as Element of T by Lm1;
B: the multF of T . (a,b) = a1 * b1
.= b1 * a1 by GROUP_1:def 12
.= the multF of T . (b,a) ;
thus a * b = (multemb f) . (x,y) by defemb
.= multemb (f,x,y) by defmult
.= (f ") . (a1 * b1) by A, defmultf
.= multemb (f,y,x) by A, B, defmultf
.= (multemb f) . (y,x) by defmult
.= b * a by defemb ; :: thesis: verum

end;

suppose A: ( not x in [#] K & not y in [#] K & not the multF of T . (x,y) in rng f ) ; :: thesis: b₁ * b₂ = b₂ * b₁

then reconsider a1 = a, b1 = b as Element of T by Lm1;
C: ( a <> 0. K & b <> 0. K ) by A;
B: the multF of T . (a,b) = a1 * b1
.= b1 * a1 by GROUP_1:def 12
.= the multF of T . (b,a) ;
thus a * b = (multemb f) . (x,y) by defemb
.= multemb (f,x,y) by defmult
.= the multF of T . (a,b) by C, A, defmultf
.= multemb (f,y,x) by C, A, B, defmultf
.= (multemb f) . (y,x) by defmult
.= b * a by defemb ; :: thesis: verum

end;

end;

end;

hence embField f is commutative ; :: thesis: verum

end;

thus embField f is well-unital :: thesis: verum

proof

now :: thesis: for a being Element of (embField f) holds
( a * (1. (embField f)) = a & (1. (embField f)) * a = a )

let a be Element of (embField f); :: thesis: ( b₁ * (1. (embField f)) = b₁ & (1. (embField f)) * b₁ = b₁ )
reconsider x = a as Element of carr f by defemb;
reconsider e = 1. (embField f) as Element of carr f by defemb;
B: a * (1. (embField f)) = (multemb f) . (x,e) by defemb
.= multemb (f,x,e) by defmult ;
D: (1. (embField f)) * a = (multemb f) . (e,x) by defemb
.= multemb (f,e,x) by defmult ;
C: 1. (embField f) = 1. K by defemb;

per cases ( x in [#] K or not x in [#] K ) ;

suppose x in [#] K ; :: thesis: ( b₁ * (1. (embField f)) = b₁ & (1. (embField f)) * b₁ = b₁ )

then reconsider a1 = a as Element of K ;
multemb (f,x,e) = a1 * (1. K) by C, defmultf;
hence a * (1. (embField f)) = a by B; :: thesis: (1. (embField f)) * a = a
multemb (f,e,x) = (1. K) * a1 by C, defmultf;
hence (1. (embField f)) * a = a by D; :: thesis: verum

end;

suppose A: not x in [#] K ; :: thesis: ( b₁ * (1. (embField f)) = b₁ & (1. (embField f)) * b₁ = b₁ )

then reconsider a1 = a as Element of T by Lm1;
E: ( e in [#] K & e <> 0. K ) by C;
then multemb (f,x,e) = the multF of T . (a1,(f . e)) by A, defmultf
.= the multF of T . (a1,(f . (1_ K))) by defemb
.= a1 * (1_ T) by GROUP_1:def 13 ;
hence a * (1. (embField f)) = a by B; :: thesis: (1. (embField f)) * a = a
multemb (f,e,x) = the multF of T . ((f . e),a1) by E, A, defmultf
.= the multF of T . ((f . (1_ K)),a1) by defemb
.= (1_ T) * a1 by GROUP_1:def 13 ;
hence (1. (embField f)) * a = a by D; :: thesis: verum

end;

end;

end;

hence embField f is well-unital ; :: thesis: verum

end;