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:28;
reconsider G = g2 * g1 as directed-sups-preserving Function of T1,T3 by WAYBEL20:28;
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
g1 * h is directed-sups-preserving Function of S3,T2 by WAYBEL20:28;
then reconsider ghf = (g1 * h) * f1 as directed-sups-preserving Function of S2,T2 by WAYBEL20:28;
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 ((UPS (f2,g2)) * (UPS (f1,g1))) . h = (UPS (f2,g2)) . ((UPS (f1,g1)) . h) by FUNCT_1:13
.= (UPS (f2,g2)) . ((g1 * h) * f1) by Def5 ;
hence ((UPS (f2,g2)) * (UPS (f1,g1))) . h = (g2 * ghf) * f2 by Def5
.= g2 * (((g1 * h) * f1) * f2) by RELAT_1:36
.= g2 * ((g1 * (h * f1)) * f2) by RELAT_1:36
.= g2 * (g1 * ((h * f1) * f2)) by RELAT_1:36
.= g2 * (g1 * (h * (f1 * f2))) by RELAT_1:36
.= g2 * ((g1 * h) * (f1 * f2)) by RELAT_1:36
.= (g2 * (g1 * h)) * (f1 * f2) by RELAT_1:36
.= (G * h) * F by RELAT_1:36 ;
:: thesis: verum

end;

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