defpred S1[ 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 S1[x,y]
proof
let x be
Element of
(UPS (S2,T1));
ex y being Element of (UPS (S1,T2)) st S1[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
;
S1[x,y]
thus
S1[
x,
y]
;
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 S1[x,j . x]
from FUNCT_2:sch 3(A3);
reconsider F = j as Function of (UPS (S2,T1)),(UPS (S1,T2)) ;
take
F
; 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; F . h = (g * h) * f
h is Element of (UPS (S2,T1))
by Def4;
hence
F . h = (g * h) * f
by A4; verum