let A, B be non empty transitive with_units AltCatStr ; :: thesis: for F being covariant Functor of A,B

for o1, o2 being Object of A

for a being Morphism of o1,o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is coretraction holds

F . a is coretraction

let F be covariant Functor of A,B; :: thesis: for o1, o2 being Object of A

for a being Morphism of o1,o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is coretraction holds

F . a is coretraction

let o1, o2 be Object of A; :: thesis: for a being Morphism of o1,o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is coretraction holds

F . a is coretraction

let a be Morphism of o1,o2; :: thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is coretraction implies F . a is coretraction )

assume A1: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) ; :: thesis: ( not a is coretraction or F . a is coretraction )

assume a is coretraction ; :: thesis: F . a is coretraction

then consider b being Morphism of o2,o1 such that

A2: a is_right_inverse_of b ;

take F . b ; :: according to ALTCAT_3:def 3 :: thesis: F . b is_left_inverse_of F . a

b * a = idm o1 by A2;

hence (F . b) * (F . a) = F . (idm o1) by A1, FUNCTOR0:def 23

.= idm (F . o1) by FUNCTOR2:1 ;

:: according to ALTCAT_3:def 1 :: thesis: verum

for o1, o2 being Object of A

for a being Morphism of o1,o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is coretraction holds

F . a is coretraction

let F be covariant Functor of A,B; :: thesis: for o1, o2 being Object of A

for a being Morphism of o1,o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is coretraction holds

F . a is coretraction

let o1, o2 be Object of A; :: thesis: for a being Morphism of o1,o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is coretraction holds

F . a is coretraction

let a be Morphism of o1,o2; :: thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is coretraction implies F . a is coretraction )

assume A1: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) ; :: thesis: ( not a is coretraction or F . a is coretraction )

assume a is coretraction ; :: thesis: F . a is coretraction

then consider b being Morphism of o2,o1 such that

A2: a is_right_inverse_of b ;

take F . b ; :: according to ALTCAT_3:def 3 :: thesis: F . b is_left_inverse_of F . a

b * a = idm o1 by A2;

hence (F . b) * (F . a) = F . (idm o1) by A1, FUNCTOR0:def 23

.= idm (F . o1) by FUNCTOR2:1 ;

:: according to ALTCAT_3:def 1 :: thesis: verum