let a, b, c be object of (W -INF_category ); :: thesis: ( 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 A3:
( <^a,b^> <> {} & <^b,c^> <> {} )
; :: thesis: 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; :: thesis: 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; :: thesis: ( S2[a,b,f] & S2[b,c,g] implies S2[a,c,g * f] )
A4:
<^a,c^> <> {}
by A3, ALTCAT_1:def 4;
then
( @ f = f & @ g = g & @ (g * f) = g * f )
by A3, YELLOW21:def 7;
then
@ (g * f) = (@ g) * (@ f)
by A3, A4, ALTCAT_1:def 14;
hence
( S2[a,b,f] & S2[b,c,g] implies S2[a,c,g * f] )
by WAYBEL20:29; :: thesis: verum