thus
embField f is Abelian
embField f is right_zeroed proof
now for a, b being Element of (embField f) holds a + b = b + alet a,
b be
Element of
(embField f);
b1 + b2 = b2 + b1reconsider 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 A4:
( not
x in [#] K & not
y in [#] K & the
addF of
T . (
x,
y)
in rng f )
;
b1 + b2 = b2 + b1then 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
;
verum end; suppose A5:
( not
x in [#] K & not
y in [#] K & not the
addF of
T . (
x,
y)
in rng f )
;
b1 + b2 = b2 + b1then 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
;
verum end; end; end;
hence
embField f is
Abelian
;
verum
end;
hence
embField f is right_zeroed
; verum