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

proof

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

proof

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

end;

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

end;

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

proof

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

end;

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