let M be AbGroup; End_Ring M is right_complementable
for f being Element of (End_Ring M) holds f is right_complementable
proof
let f be
Element of
(End_Ring M);
f is right_complementable
reconsider f0 =
f as
Element of
set_End M ;
reconsider g =
Inv f0 as
Element of
(End_Ring M) ;
g in set_End M
;
then consider g1 being
Function of the
carrier of
M, the
carrier of
M such that A1:
(
g1 = g &
g1 is
Endomorphism of
M )
;
f in set_End M
;
then consider f1 being
Function of the
carrier of
M, the
carrier of
M such that A2:
(
f1 = f &
f1 is
Endomorphism of
M )
;
reconsider z1 =
0_End M as
additive Function of the
carrier of
M, the
carrier of
M ;
reconsider f1 =
f1,
z1 =
z1 as
Element of
Funcs ( the
carrier of
M, the
carrier of
M)
by A2, Th3;
A3:
f + g =
(ADD (M,M)) . (
f0,
(Inv f0))
by A2, A1, Th3
.=
0_End M
by Th7
;
take
g
;
ALGSTR_0:def 11 f + g = 0. (End_Ring M)
thus
f + g = 0. (End_Ring M)
by A3;
verum
end;
hence
End_Ring M is right_complementable
; verum