let C be category; :: thesis: for D being non empty full 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 n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {} holds

( ( m is retraction implies n is retraction ) & ( m is coretraction implies n is coretraction ) & ( m is iso implies n is iso ) )

let D be non empty full 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 n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {} holds

( ( m is retraction implies n is retraction ) & ( m is coretraction implies n is coretraction ) & ( m is iso implies n is iso ) )

let o1, o2 be Object of C; :: thesis: for p1, p2 being Object of D

for m being Morphism of o1,o2

for n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {} holds

( ( m is retraction implies n is retraction ) & ( m is coretraction implies n is coretraction ) & ( m is iso implies n is iso ) )

let p1, p2 be Object of D; :: thesis: for m being Morphism of o1,o2

for n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {} holds

( ( m is retraction implies n is retraction ) & ( m is coretraction implies n is coretraction ) & ( m is iso implies n is iso ) )

let m be Morphism of o1,o2; :: thesis: for n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {} holds

( ( m is retraction implies n is retraction ) & ( m is coretraction implies n is coretraction ) & ( m is iso implies n is iso ) )

let n be Morphism of p1,p2; :: thesis: ( p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {} implies ( ( m is retraction implies n is retraction ) & ( m is coretraction implies n is coretraction ) & ( m is iso implies n is iso ) ) )

assume that

A1: ( p1 = o1 & p2 = o2 ) and

A2: m = n and

A3: ( <^p1,p2^> <> {} & <^p2,p1^> <> {} ) ; :: thesis: ( ( m is retraction implies n is retraction ) & ( m is coretraction implies n is coretraction ) & ( m is iso implies n is iso ) )

thus A4: ( m is retraction implies n is retraction ) :: thesis: ( ( m is coretraction implies n is coretraction ) & ( m is iso implies n is iso ) )

hence n is iso by A3, A4, A6, ALTCAT_3:5, ALTCAT_3:6; :: thesis: verum

for o1, o2 being Object of C

for p1, p2 being Object of D

for m being Morphism of o1,o2

for n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {} holds

( ( m is retraction implies n is retraction ) & ( m is coretraction implies n is coretraction ) & ( m is iso implies n is iso ) )

let D be non empty full 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 n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {} holds

( ( m is retraction implies n is retraction ) & ( m is coretraction implies n is coretraction ) & ( m is iso implies n is iso ) )

let o1, o2 be Object of C; :: thesis: for p1, p2 being Object of D

for m being Morphism of o1,o2

for n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {} holds

( ( m is retraction implies n is retraction ) & ( m is coretraction implies n is coretraction ) & ( m is iso implies n is iso ) )

let p1, p2 be Object of D; :: thesis: for m being Morphism of o1,o2

for n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {} holds

( ( m is retraction implies n is retraction ) & ( m is coretraction implies n is coretraction ) & ( m is iso implies n is iso ) )

let m be Morphism of o1,o2; :: thesis: for n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {} holds

( ( m is retraction implies n is retraction ) & ( m is coretraction implies n is coretraction ) & ( m is iso implies n is iso ) )

let n be Morphism of p1,p2; :: thesis: ( p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {} implies ( ( m is retraction implies n is retraction ) & ( m is coretraction implies n is coretraction ) & ( m is iso implies n is iso ) ) )

assume that

A1: ( p1 = o1 & p2 = o2 ) and

A2: m = n and

A3: ( <^p1,p2^> <> {} & <^p2,p1^> <> {} ) ; :: thesis: ( ( m is retraction implies n is retraction ) & ( m is coretraction implies n is coretraction ) & ( m is iso implies n is iso ) )

thus A4: ( m is retraction implies n is retraction ) :: thesis: ( ( m is coretraction implies n is coretraction ) & ( m is iso implies n is iso ) )

proof

thus A6:
( m is coretraction implies n is coretraction )
:: thesis: ( m is iso implies n is iso )
assume
m is retraction
; :: thesis: n is retraction

then consider B being Morphism of o2,o1 such that

A5: B is_right_inverse_of m ;

reconsider B1 = B as Morphism of p2,p1 by A1, ALTCAT_2:28;

take B1 ; :: according to ALTCAT_3:def 2 :: thesis: n is_left_inverse_of B1

thus n is_left_inverse_of B1 by A1, A2, A3, A5, Th38; :: thesis: verum

end;then consider B being Morphism of o2,o1 such that

A5: B is_right_inverse_of m ;

reconsider B1 = B as Morphism of p2,p1 by A1, ALTCAT_2:28;

take B1 ; :: according to ALTCAT_3:def 2 :: thesis: n is_left_inverse_of B1

thus n is_left_inverse_of B1 by A1, A2, A3, A5, Th38; :: thesis: verum

proof

assume
m is iso
; :: thesis: n is iso
assume
m is coretraction
; :: thesis: n is coretraction

then consider B being Morphism of o2,o1 such that

A7: B is_left_inverse_of m ;

reconsider B1 = B as Morphism of p2,p1 by A1, ALTCAT_2:28;

take B1 ; :: according to ALTCAT_3:def 3 :: thesis: B1 is_left_inverse_of n

thus B1 is_left_inverse_of n by A1, A2, A3, A7, Th38; :: thesis: verum

end;then consider B being Morphism of o2,o1 such that

A7: B is_left_inverse_of m ;

reconsider B1 = B as Morphism of p2,p1 by A1, ALTCAT_2:28;

take B1 ; :: according to ALTCAT_3:def 3 :: thesis: B1 is_left_inverse_of n

thus B1 is_left_inverse_of n by A1, A2, A3, A7, Th38; :: thesis: verum

hence n is iso by A3, A4, A6, ALTCAT_3:5, ALTCAT_3:6; :: thesis: verum