let M be AbGroup; End_Ring M is add-associative
for f, g, h being Element of (End_Ring M) holds f + (g + h) = (f + g) + h
proof
let f,
g,
h be
Element of
(End_Ring M);
f + (g + h) = (f + g) + h
reconsider fg =
f + g,
gh =
g + h as
Element of
set_End M ;
reconsider f1 =
f,
g1 =
g,
h1 =
h,
fg1 =
fg,
gh1 =
gh as
Endomorphism of
M by Lm3;
reconsider f1 =
f1,
g1 =
g1,
h1 =
h1,
fg1 =
fg1,
gh1 =
gh1 as
Element of
Funcs ( the
carrier of
M, the
carrier of
M)
by Th3;
A1:
(ADD (M,M)) . (
f1,
g1)
= fg
by Th3;
A2:
(ADD (M,M)) . (
g1,
h1)
= gh
by Th3;
(f + g) + h =
(ADD (M,M)) . (
fg1,
h1)
by Th3
.=
(ADD (M,M)) . (
f1,
gh1)
by A2, A1, Lm2
.=
f + (g + h)
by Th3
;
hence
f + (g + h) = (f + g) + h
;
verum
end;
hence
End_Ring M is add-associative
; verum