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 A1: ( p1 = o1 & p2 = o2 & 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 A2: m is_left_inverse_of m1 ; :: thesis:
thus n * n1 = m * m1 by A1, ALTCAT_2:33
.= idm o2 by A2, ALTCAT_3:def 1
.= idm p2 by A1, ALTCAT_2:35 ; :: according to ALTCAT_3:def 1 :: thesis:

end;

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

end;

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

assume A4: m is_right_inverse_of m1 ; :: thesis:
thus n1 * n = m1 * m by A1, ALTCAT_2:33
.= idm o1 by A4, ALTCAT_3:def 1
.= idm p1 by A1, ALTCAT_2:35 ; :: according to ALTCAT_3:def 1 :: thesis:

end;

assume A5: n is_right_inverse_of n1 ; :: thesis:
thus m1 * m = n1 * n by A1, ALTCAT_2:33
.= idm p1 by A5, ALTCAT_3:def 1
.= idm o1 by A1, ALTCAT_2:35 ; :: according to ALTCAT_3:def 1 :: thesis: