let C be category; :: thesis: for D being non empty subcategory of C
for o1, o2 being Object of C
for p1, p2 being Object of D
for m being Morphism of o1,o2
for m1 being Morphism of o2,o1
for n being Morphism of p1,p2
for n1 being Morphism of p2,p1 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 C; :: thesis: for o1, o2 being Object of C
for p1, p2 being Object of D
for m being Morphism of o1,o2
for m1 being Morphism of o2,o1
for n being Morphism of p1,p2
for n1 being Morphism of p2,p1 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 C; :: thesis: for p1, p2 being Object of D
for m being Morphism of o1,o2
for m1 being Morphism of o2,o1
for n being Morphism of p1,p2
for n1 being Morphism of p2,p1 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 D; :: thesis: for m being Morphism of o1,o2
for m1 being Morphism of o2,o1
for n being Morphism of p1,p2
for n1 being Morphism of p2,p1 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 o1,o2; :: thesis: for m1 being Morphism of o2,o1
for n being Morphism of p1,p2
for n1 being Morphism of p2,p1 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 o2,o1; :: thesis: for n being Morphism of p1,p2
for n1 being Morphism of p2,p1 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 p1,p2; :: thesis: for n1 being Morphism of p2,p1 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 p2,p1; :: 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:32
.= idm o2 by A4
.= idm p2 by A2, ALTCAT_2:34 ; :: 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:32
.= idm p2 by A5
.= idm o2 by A2, ALTCAT_2:34 ; :: 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:32
.= idm o1 by A6
.= idm p1 by A1, ALTCAT_2:34 ; :: 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:32
.= idm p1 by A7
.= idm o1 by A1, ALTCAT_2:34 ; :: according to ALTCAT_3:def 1 :: thesis: verum