let A, B be non empty transitive with_units AltCatStr ; 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 retraction holds
F . a is retraction
let F be 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 retraction holds
F . a is retraction
let o1, o2 be Object of A; for a being Morphism of o1,o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is retraction holds
F . a is retraction
let a be Morphism of o1,o2; ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is retraction implies F . a is retraction )
assume A1:
( <^o1,o2^> <> {} & <^o2,o1^> <> {} )
; ( not a is retraction or F . a is retraction )
assume
a is retraction
; F . a is retraction
then consider b being Morphism of o2,o1 such that
A2:
b is_right_inverse_of a
;
take
F . b
; ALTCAT_3:def 2 F . a is_left_inverse_of F . b
a * b = idm o2
by A2;
hence (F . a) * (F . b) =
F . (idm o2)
by A1, FUNCTOR0:def 23
.=
idm (F . o2)
by FUNCTOR2:1
;
ALTCAT_3:def 1 verum