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

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

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

( ( n is retraction implies m is retraction ) & ( n is coretraction implies m is coretraction ) & ( n is iso implies m 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

( ( n is retraction implies m is retraction ) & ( n is coretraction implies m is coretraction ) & ( n is iso implies m 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

( ( n is retraction implies m is retraction ) & ( n is coretraction implies m is coretraction ) & ( n is iso implies m 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

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

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

assume that

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

A2: m = n and

A3: <^p1,p2^> <> {} and

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

A5: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) by A1, A3, A4, ALTCAT_2:31, XBOOLE_1:3;

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

hence m is iso by A6, A8, A5, 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

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

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

( ( n is retraction implies m is retraction ) & ( n is coretraction implies m is coretraction ) & ( n is iso implies m 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

( ( n is retraction implies m is retraction ) & ( n is coretraction implies m is coretraction ) & ( n is iso implies m 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

( ( n is retraction implies m is retraction ) & ( n is coretraction implies m is coretraction ) & ( n is iso implies m 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

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

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

assume that

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

A2: m = n and

A3: <^p1,p2^> <> {} and

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

A5: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) by A1, A3, A4, ALTCAT_2:31, XBOOLE_1:3;

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

proof

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

then consider B being Morphism of p2,p1 such that

A7: B is_right_inverse_of n ;

reconsider B1 = B as Morphism of o2,o1 by A1, A4, ALTCAT_2:33;

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

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

end;then consider B being Morphism of p2,p1 such that

A7: B is_right_inverse_of n ;

reconsider B1 = B as Morphism of o2,o1 by A1, A4, ALTCAT_2:33;

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

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

proof

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

then consider B being Morphism of p2,p1 such that

A9: B is_left_inverse_of n ;

reconsider B1 = B as Morphism of o2,o1 by A1, A4, ALTCAT_2:33;

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

thus B1 is_left_inverse_of m by A1, A2, A3, A4, A9, Th38; :: thesis: verum

end;then consider B being Morphism of p2,p1 such that

A9: B is_left_inverse_of n ;

reconsider B1 = B as Morphism of o2,o1 by A1, A4, ALTCAT_2:33;

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

thus B1 is_left_inverse_of m by A1, A2, A3, A4, A9, Th38; :: thesis: verum

hence m is iso by A6, A8, A5, ALTCAT_3:5, ALTCAT_3:6; :: thesis: verum