let M be AbGroup; End_Ring M is Abelian
for f, g being Element of (End_Ring M) holds f + g = g + f
proof
let f,
g be
Element of
(End_Ring M);
f + g = g + f
f in set_End M
;
then consider f1 being
Function of the
carrier of
M, the
carrier of
M such that A1:
(
f1 = f &
f1 is
Endomorphism of
M )
;
g in set_End M
;
then consider g1 being
Function of the
carrier of
M, the
carrier of
M such that A2:
(
g1 = g &
g1 is
Endomorphism of
M )
;
reconsider f1 =
f1,
g1 =
g1 as
Element of
Funcs ( the
carrier of
M, the
carrier of
M)
by FUNCT_2:9;
f + g =
(ADD (M,M)) . (
f1,
g1)
by A1, A2, Th3
.=
(ADD (M,M)) . (
g1,
f1)
by Th4
.=
g + f
by A1, A2, Th3
;
hence
f + g = g + f
;
verum
end;
hence
End_Ring M is Abelian
; verum