let C be category; for o1, o2, o3 being Object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} holds
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is coretraction & B is coretraction holds
B * A is coretraction
let o1, o2, o3 be Object of C; ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} implies for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is coretraction & B is coretraction holds
B * A is coretraction )
assume that
A1:
<^o1,o2^> <> {}
and
A2:
<^o2,o3^> <> {}
and
A3:
<^o3,o1^> <> {}
; for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is coretraction & B is coretraction holds
B * A is coretraction
A4:
<^o2,o1^> <> {}
by A2, A3, ALTCAT_1:def 2;
A5:
<^o3,o2^> <> {}
by A1, A3, ALTCAT_1:def 2;
let A be Morphism of o1,o2; for B being Morphism of o2,o3 st A is coretraction & B is coretraction holds
B * A is coretraction
let B be Morphism of o2,o3; ( A is coretraction & B is coretraction implies B * A is coretraction )
assume that
A6:
A is coretraction
and
A7:
B is coretraction
; B * A is coretraction
consider A1 being Morphism of o2,o1 such that
A8:
A1 is_left_inverse_of A
by A6;
consider B1 being Morphism of o3,o2 such that
A9:
B1 is_left_inverse_of B
by A7;
consider G being Morphism of o3,o1 such that
A10:
G = A1 * B1
;
take
G
; ALTCAT_3:def 3 G is_left_inverse_of B * A
A11:
<^o2,o2^> <> {}
by ALTCAT_1:19;
G * (B * A) =
((A1 * B1) * B) * A
by A1, A2, A3, A10, ALTCAT_1:21
.=
(A1 * (B1 * B)) * A
by A2, A4, A5, ALTCAT_1:21
.=
(A1 * (idm o2)) * A
by A9
.=
A1 * ((idm o2) * A)
by A1, A4, A11, ALTCAT_1:21
.=
A1 * A
by A1, ALTCAT_1:20
.=
idm o1
by A8
;
hence
G is_left_inverse_of B * A
; verum