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 retraction & B is retraction holds
B * A is retraction
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 retraction & B is retraction holds
B * A is retraction )
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 retraction & B is retraction holds
B * A is retraction
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 retraction & B is retraction holds
B * A is retraction
let B be Morphism of o2,o3; ( A is retraction & B is retraction implies B * A is retraction )
assume that
A6:
A is retraction
and
A7:
B is retraction
; B * A is retraction
consider A1 being Morphism of o2,o1 such that
A8:
A1 is_right_inverse_of A
by A6;
consider B1 being Morphism of o3,o2 such that
A9:
B1 is_right_inverse_of B
by A7;
consider G being Morphism of o3,o1 such that
A10:
G = A1 * B1
;
take
G
; ALTCAT_3:def 2 G is_right_inverse_of B * A
(B * A) * G =
B * (A * (A1 * B1))
by A1, A2, A3, A10, ALTCAT_1:21
.=
B * ((A * A1) * B1)
by A1, A4, A5, ALTCAT_1:21
.=
B * ((idm o2) * B1)
by A8
.=
B * B1
by A5, ALTCAT_1:20
.=
idm o3
by A9
;
hence
G is_right_inverse_of B * A
; verum