let C be category; for o1, o2, o3 being Object of C
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is coretraction holds
A is coretraction
let o1, o2, o3 be Object of C; for A being Morphism of o1,o2
for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is coretraction holds
A is coretraction
let A be Morphism of o1,o2; for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is coretraction holds
A is coretraction
let B be Morphism of o2,o3; ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is coretraction implies A is coretraction )
assume A1:
( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} )
; ( not B * A is coretraction or A is coretraction )
assume
B * A is coretraction
; A is coretraction
then consider G being Morphism of o3,o1 such that
A2:
G is_left_inverse_of B * A
;
A3:
(G * B) * A = G * (B * A)
by A1, ALTCAT_1:21;
G * (B * A) = idm o1
by A2;
then
G * B is_left_inverse_of A
by A3;
hence
A is coretraction
; verum