defpred S₁[ set , set ] means for h being Function st h = $1 holds
$2 = (g * h) * f;
A3: for x being Element of (UPS (S2,T1)) ex y being Element of (UPS (S1,T2)) st S₁[x,y]

proof

let x be Element of (UPS (S2,T1)); :: thesis: ex y being Element of (UPS (S1,T2)) st S₁[x,y]
reconsider h = x as directed-sups-preserving Function of S2,T1 by Def4;
h * f is directed-sups-preserving Function of S1,T1 by A1, WAYBEL20:28;
then g * (h * f) is directed-sups-preserving Function of S1,T2 by A2, WAYBEL20:28;
then (g * h) * f is directed-sups-preserving Function of S1,T2 by RELAT_1:36;
then reconsider y = (g * h) * f as Element of (UPS (S1,T2)) by Def4;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

consider j being Function of the carrier of (UPS (S2,T1)), the carrier of (UPS (S1,T2)) such that
A4: for x being Element of (UPS (S2,T1)) holds S₁[x,j . x] from FUNCT_2:sch 3(A3);
reconsider F = j as Function of (UPS (S2,T1)),(UPS (S1,T2)) ;
take F ; :: thesis: for h being directed-sups-preserving Function of S2,T1 holds F . h = (g * h) * f
let h be directed-sups-preserving Function of S2,T1; :: thesis: F . h = (g * h) * f
h is Element of (UPS (S2,T1)) by Def4;
hence F . h = (g * h) * f by A4; :: thesis: verum