let C be category; :: thesis:
let D be non empty subcategory of C; :: thesis:
let o1, o2 be Object of C; :: thesis:
let p1, p2 be Object of D; :: thesis:
let m be Morphism of o1,o2; :: thesis:
let m1 be Morphism of o2,o1; :: thesis:
let n be Morphism of p1,p2; :: thesis:
let n1 be Morphism of p2,p1; :: thesis:
assume that
A1: p1 = o1 and
A2: p2 = o2 and
A3: ( m = n & m1 = n1 & <^p1,p2^> <> {} & <^p2,p1^> <> {} ) ; :: thesis:
thus ( m is_left_inverse_of m1 iff n is_left_inverse_of n1 ) :: thesis:

thus ( m is_left_inverse_of m1 implies n is_left_inverse_of n1 ) :: thesis:

assume A4: m is_left_inverse_of m1 ; :: thesis:
thus n * n1 = m * m1 by A1, A2, A3, ALTCAT_2:32
.= idm o2 by A4
.= idm p2 by A2, ALTCAT_2:34 ; :: according to ALTCAT_3:def 1 :: thesis:

end;

assume A5: n is_left_inverse_of n1 ; :: thesis:
thus m * m1 = n * n1 by A1, A2, A3, ALTCAT_2:32
.= idm p2 by A5
.= idm o2 by A2, ALTCAT_2:34 ; :: according to ALTCAT_3:def 1 :: thesis:

end;

thus ( m is_right_inverse_of m1 implies n is_right_inverse_of n1 ) :: thesis:

assume A6: m is_right_inverse_of m1 ; :: thesis:
thus n1 * n = m1 * m by A1, A2, A3, ALTCAT_2:32
.= idm o1 by A6
.= idm p1 by A1, ALTCAT_2:34 ; :: according to ALTCAT_3:def 1 :: thesis:

end;

assume A7: n is_right_inverse_of n1 ; :: thesis:
thus m1 * m = n1 * n by A1, A2, A3, ALTCAT_2:32
.= idm p1 by A7
.= idm o1 by A1, ALTCAT_2:34 ; :: according to ALTCAT_3:def 1 :: thesis: