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

proof

let x be Element of ; :: thesis: ex y being Element of 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:29;
then g * (h * f) is directed-sups-preserving Function of S1,T2 by A2, WAYBEL20:29;
then (g * h) * f is directed-sups-preserving Function of S1,T2 by RELAT_1:55;
then reconsider y = (g * h) * f as Element of 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 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 by Def4;
hence F . h = (g * h) * f by A4; :: thesis: verum