let a, b, c be object of (W -INF_category); ( S1[a] & S1[b] & S1[c] & <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c st S2[a,b,f] & S2[b,c,g] holds
S2[a,c,g * f] )
assume that
A3:
<^a,b^> <> {}
and
A4:
<^b,c^> <> {}
; for f being Morphism of a,b
for g being Morphism of b,c st S2[a,b,f] & S2[b,c,g] holds
S2[a,c,g * f]
let f be Morphism of a,b; for g being Morphism of b,c st S2[a,b,f] & S2[b,c,g] holds
S2[a,c,g * f]
let g be Morphism of b,c; ( S2[a,b,f] & S2[b,c,g] implies S2[a,c,g * f] )
A5:
<^a,c^> <> {}
by A3, A4, ALTCAT_1:def 4;
A6:
@ f = f
by A3, YELLOW21:def 7;
A7:
@ g = g
by A4, YELLOW21:def 7;
@ (g * f) = g * f
by A5, YELLOW21:def 7;
then
@ (g * f) = (@ g) * (@ f)
by A3, A4, A5, A6, A7, ALTCAT_1:def 14;
hence
( S2[a,b,f] & S2[b,c,g] implies S2[a,c,g * f] )
by WAYBEL20:29; verum