let M1, M2 be Morphism of o2,o1; ( M1 is_left_inverse_of A & M1 is_right_inverse_of A & M2 is_left_inverse_of A & M2 is_right_inverse_of A implies M1 = M2 )
assume that
A3:
M1 is_left_inverse_of A
and
M1 is_right_inverse_of A
and
M2 is_left_inverse_of A
and
A4:
M2 is_right_inverse_of A
; M1 = M2
thus M1 =
M1 * (idm o2)
by B2, ALTCAT_1:def 17
.=
M1 * (A * M2)
by A4, Def1
.=
(M1 * A) * M2
by B1, B2, ALTCAT_1:21
.=
(idm o1) * M2
by A3, Def1
.=
M2
by B2, ALTCAT_1:20
; verum