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
A6:
M1 is_left_inverse_of A
and
M1 is_right_inverse_of A
and
M2 is_left_inverse_of A
and
A7:
M2 is_right_inverse_of A
; M1 = M2
thus M1 =
M1 * (idm o2)
by A2, ALTCAT_1:def 17
.=
M1 * (A * M2)
by A7
.=
(M1 * A) * M2
by A1, A2, ALTCAT_1:21
.=
(idm o1) * M2
by A6
.=
M2
by A2, ALTCAT_1:20
; verum