theorem Th28:
for
S1,
S2,
S3,
T1,
T2,
T3 being non
empty Poset for
f1 being
directed-sups-preserving Function of
S2,
S3 for
f2 being
directed-sups-preserving Function of
S1,
S2 for
g1 being
directed-sups-preserving Function of
T1,
T2 for
g2 being
directed-sups-preserving Function of
T2,
T3 holds
(UPS (f2,g2)) * (UPS (f1,g1)) = UPS (
(f1 * f2),
(g2 * g1))