thus embField f is Abelian :: thesis: embField f is right_zeroed

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 ( x in [#] K & not y in [#] K ) or ( y in [#] K & not x in [#] K ) or ( not x in [#] K & not y in [#] K & the addF of T . (x,y) in rng f ) or ( not x in [#] K & not y in [#] K & not the addF 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 Lm7
.= b + a by Lm7 ; :: thesis: verum

end;

suppose A2: ( x in [#] 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 A2, Lm1;
reconsider fa = f . a1 as Element of T ;
thus a + b = (addemb f) . (x,y) by defemb
.= addemb (f,x,y) by defadd
.= fa + b1 by A2, defaddf
.= b1 + fa
.= addemb (f,y,x) by A2, defaddf
.= (addemb f) . (y,x) by defadd
.= b + a by defemb ; :: thesis: verum

end;

suppose A3: ( y in [#] 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 A3, Lm1;
reconsider fb = f . b1 as Element of T ;
thus a + b = (addemb f) . (x,y) by defemb
.= addemb (f,x,y) by defadd
.= a1 + fb by A3, defaddf
.= fb + a1
.= addemb (f,y,x) by A3, defaddf
.= (addemb f) . (y,x) by defadd
.= b + a by defemb ; :: thesis: verum

end;

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

then reconsider a1 = a, b1 = b as Element of T by Lm1;
B1: the addF of T . (a,b) = a1 + b1
.= b1 + a1
.= the addF of T . (b,a) ;
thus a + b = (addemb f) . (x,y) by defemb
.= addemb (f,x,y) by defadd
.= (f ") . (a1 + b1) by A4, defaddf
.= addemb (f,y,x) by A4, B1, defaddf
.= (addemb f) . (y,x) by defadd
.= b + a by defemb ; :: thesis: verum

end;

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

then reconsider a1 = a, b1 = b as Element of T by Lm1;
B2: the addF of T . (a,b) = a1 + b1
.= b1 + a1
.= the addF of T . (b,a) ;
thus a + b = (addemb f) . (x,y) by defemb
.= addemb (f,x,y) by defadd
.= a1 + b1 by A5, defaddf
.= addemb (f,y,x) by A5, B2, defaddf
.= (addemb f) . (y,x) by defadd
.= b + a by defemb ; :: thesis: verum

end;

end;

end;

hence embField f is Abelian ; :: thesis: verum

end;

now :: thesis: for a being Element of (embField f) holds a + (0. (embField f)) = a

let a be Element of (embField f); :: thesis: b₁ + (0. (embField f)) = b₁
reconsider x = a as Element of carr f by defemb;
reconsider o = 0. (embField f) as Element of carr f by defemb;
B1: a + (0. (embField f)) = (addemb f) . (x,o) by defemb
.= addemb (f,x,o) by defadd ;
C1: 0. (embField f) = 0. K by defemb;

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

suppose x in [#] K ; :: thesis: b₁ + (0. (embField f)) = b₁

then reconsider a1 = a as Element of K ;
addemb (f,x,o) = a1 + (0. K) by C1, defaddf;
hence a + (0. (embField f)) = a by B1; :: thesis: verum

end;

suppose A1: not x in [#] K ; :: thesis: b₁ + (0. (embField f)) = b₁

then reconsider a1 = a as Element of T by Lm1;
addemb (f,x,o) = the addF of T . (a,(f . o)) by A1, C1, defaddf
.= a1 + (0. T) by C1, RING_2:6 ;
hence a + (0. (embField f)) = a by B1; :: thesis: verum

end;

end;

end;

hence embField f is right_zeroed ; :: thesis: verum