let C be category; :: thesis: for o1, o2 being Object of (AllIso C)

for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

( m is iso & m " in <^o2,o1^> )

let o1, o2 be Object of (AllIso C); :: thesis: for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

( m is iso & m " in <^o2,o1^> )

let m be Morphism of o1,o2; :: thesis: ( <^o1,o2^> <> {} implies ( m is iso & m " in <^o2,o1^> ) )

assume A1: <^o1,o2^> <> {} ; :: thesis: ( m is iso & m " in <^o2,o1^> )

reconsider p1 = o1, p2 = o2 as Object of C by Def5;

reconsider p = m as Morphism of p1,p2 by A1, ALTCAT_2:33;

p in the Arrows of (AllIso C) . (o1,o2) by A1;

then A2: ( <^p1,p2^> <> {} & <^p2,p1^> <> {} ) by Def5;

A3: p is iso by A1, Def5;

then A4: p " is iso by A2, Th3;

then A5: p " in the Arrows of (AllIso C) . (p2,p1) by A2, Def5;

reconsider m1 = p " as Morphism of o2,o1 by A2, A4, Def5;

A6: m is retraction

hence m is iso by A1, A6, A7, ALTCAT_3:6; :: thesis: m " in <^o2,o1^>

thus m " in <^o2,o1^> by A5; :: thesis: verum

for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

( m is iso & m " in <^o2,o1^> )

let o1, o2 be Object of (AllIso C); :: thesis: for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

( m is iso & m " in <^o2,o1^> )

let m be Morphism of o1,o2; :: thesis: ( <^o1,o2^> <> {} implies ( m is iso & m " in <^o2,o1^> ) )

assume A1: <^o1,o2^> <> {} ; :: thesis: ( m is iso & m " in <^o2,o1^> )

reconsider p1 = o1, p2 = o2 as Object of C by Def5;

reconsider p = m as Morphism of p1,p2 by A1, ALTCAT_2:33;

p in the Arrows of (AllIso C) . (o1,o2) by A1;

then A2: ( <^p1,p2^> <> {} & <^p2,p1^> <> {} ) by Def5;

A3: p is iso by A1, Def5;

then A4: p " is iso by A2, Th3;

then A5: p " in the Arrows of (AllIso C) . (p2,p1) by A2, Def5;

reconsider m1 = p " as Morphism of o2,o1 by A2, A4, Def5;

A6: m is retraction

proof

A7:
m is coretraction
take
m1
; :: according to ALTCAT_3:def 2 :: thesis: m is_left_inverse_of m1

thus m * m1 = p * (p ") by A1, A5, ALTCAT_2:32

.= idm p2 by A3

.= idm o2 by ALTCAT_2:34 ; :: according to ALTCAT_3:def 1 :: thesis: verum

end;thus m * m1 = p * (p ") by A1, A5, ALTCAT_2:32

.= idm p2 by A3

.= idm o2 by ALTCAT_2:34 ; :: according to ALTCAT_3:def 1 :: thesis: verum

proof

p " in <^o2,o1^>
by A2, A4, Def5;
take
m1
; :: according to ALTCAT_3:def 3 :: thesis: m1 is_left_inverse_of m

thus m1 * m = (p ") * p by A1, A5, ALTCAT_2:32

.= idm p1 by A3

.= idm o1 by ALTCAT_2:34 ; :: according to ALTCAT_3:def 1 :: thesis: verum

end;thus m1 * m = (p ") * p by A1, A5, ALTCAT_2:32

.= idm p1 by A3

.= idm o1 by ALTCAT_2:34 ; :: according to ALTCAT_3:def 1 :: thesis: verum

hence m is iso by A1, A6, A7, ALTCAT_3:6; :: thesis: m " in <^o2,o1^>

thus m " in <^o2,o1^> by A5; :: thesis: verum