let S1, S2, S3, T1, T2, T3 be non empty Poset; :: thesis: 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)
let f1 be directed-sups-preserving Function of S2,S3; :: thesis: 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)
let f2 be directed-sups-preserving Function of S1,S2; :: thesis: 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)
let g1 be directed-sups-preserving Function of T1,T2; :: thesis: for g2 being directed-sups-preserving Function of T2,T3 holds (UPS f2,g2) * (UPS f1,g1) = UPS (f1 * f2),(g2 * g1)
let g2 be directed-sups-preserving Function of T2,T3; :: thesis: (UPS f2,g2) * (UPS f1,g1) = UPS (f1 * f2),(g2 * g1)
reconsider F = f1 * f2 as directed-sups-preserving Function of S1,S3 by WAYBEL20:29;
reconsider G = g2 * g1 as directed-sups-preserving Function of T1,T3 by WAYBEL20:29;
for h being directed-sups-preserving Function of S3,T1 holds ((UPS f2,g2) * (UPS f1,g1)) . h = (G * h) * F

proof

let h be directed-sups-preserving Function of S3,T1; :: thesis: ((UPS f2,g2) * (UPS f1,g1)) . h = (G * h) * F
dom (UPS f1,g1) = the carrier of (UPS S3,T1) by FUNCT_2:def 1;
then h in dom (UPS f1,g1) by Def4;
then A1: ((UPS f2,g2) * (UPS f1,g1)) . h = (UPS f2,g2) . ((UPS f1,g1) . h) by FUNCT_1:23
.= (UPS f2,g2) . ((g1 * h) * f1) by Def5 ;
g1 * h is directed-sups-preserving Function of S3,T2 by WAYBEL20:29;
then reconsider ghf = (g1 * h) * f1 as directed-sups-preserving Function of S2,T2 by WAYBEL20:29;
thus ((UPS f2,g2) * (UPS f1,g1)) . h = (g2 * ghf) * f2 by A1, Def5
.= g2 * (((g1 * h) * f1) * f2) by RELAT_1:55
.= g2 * ((g1 * (h * f1)) * f2) by RELAT_1:55
.= g2 * (g1 * ((h * f1) * f2)) by RELAT_1:55
.= g2 * (g1 * (h * (f1 * f2))) by RELAT_1:55
.= g2 * ((g1 * h) * (f1 * f2)) by RELAT_1:55
.= (g2 * (g1 * h)) * (f1 * f2) by RELAT_1:55
.= (G * h) * F by RELAT_1:55 ; :: thesis: verum

end;

hence (UPS f2,g2) * (UPS f1,g1) = UPS (f1 * f2),(g2 * g1) by Def5; :: thesis: verum