let a, b, c be object of (W -SUP_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 A4:
( <^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] )
A5:
<^a,c^> <> {}
by A4, ALTCAT_1:def 4;
then
( @ f = f & @ g = g & @ (g * f) = g * f )
by A4, YELLOW21:def 7;
then
( @ g is sups-preserving Function of (latt b),(latt c) & @ f is sups-preserving Function of (latt a),(latt b) & @ (g * f) = (@ g) * (@ f) )
by A1, A4, A5, Def5, ALTCAT_1:def 14;
then
UpperAdj (@ (g * f)) = (UpperAdj (@ f)) * (UpperAdj (@ g))
by Th9;
hence
( S2[a,b,f] & S2[b,c,g] implies S2[a,c,g * f] )
by WAYBEL20:29; :: thesis: verum