let R, S, T be complete LATTICE; :: thesis: for f being directed-sups-preserving Function of R,(UPS (S,T)) holds uncurry f is directed-sups-preserving Function of [:R,S:],T
let f be directed-sups-preserving Function of R,(UPS (S,T)); :: thesis: uncurry f is directed-sups-preserving Function of [:R,S:],T
A1: f in Funcs ( the carrier of R, the carrier of (UPS (S,T))) by FUNCT_2:8;
Funcs ( the carrier of R, the carrier of (UPS (S,T))) c= Funcs ( the carrier of R,(Funcs ( the carrier of S, the carrier of T))) by Th22, FUNCT_5:56;
then uncurry f in Funcs ([: the carrier of R, the carrier of S:], the carrier of T) by A1, FUNCT_6:11;
then uncurry f in Funcs ( the carrier of [:R,S:], the carrier of T) by YELLOW_3:def 2;
then reconsider g = uncurry f as Function of [:R,S:],T by FUNCT_2:66;
A2: the carrier of (UPS (S,T)) c= Funcs ( the carrier of S, the carrier of T) by Th22;

now :: thesis: for a being Element of R
for b being Element of S holds
( Proj (g,a) is directed-sups-preserving & Proj (g,b) is directed-sups-preserving )

reconsider ST = UPS (S,T) as non empty full sups-inheriting SubRelStr of T |^ the carrier of S by Def4, Th26;
let a be Element of R; :: thesis: for b being Element of S holds
( Proj (g,a) is directed-sups-preserving & Proj (g,b) is directed-sups-preserving )
let b be Element of S; :: thesis: ( Proj (g,a) is directed-sups-preserving & Proj (g,b) is directed-sups-preserving )
reconsider f9 = f as directed-sups-preserving Function of R,ST ;
incl (ST,(T |^ the carrier of S)) is directed-sups-preserving by WAYBEL21:10;
then A3: (incl (ST,(T |^ the carrier of S))) * f9 is directed-sups-preserving by WAYBEL20:28;
the carrier of ST c= the carrier of (T |^ the carrier of S) by YELLOW_0:def 13;
then incl (ST,(T |^ the carrier of S)) = id the carrier of ST by YELLOW_9:def 1;
then f is directed-sups-preserving Function of R,(T |^ the carrier of S) by A3, FUNCT_2:17;
then A4: (commute f) . b is directed-sups-preserving Function of R,T by Th38;
rng f c= Funcs ( the carrier of S, the carrier of T) by A2;
then curry g = f by FUNCT_5:48;
then Proj (g,a) = f . a by WAYBEL24:def 1;
hence Proj (g,a) is directed-sups-preserving by Def4; :: thesis: Proj (g,b) is directed-sups-preserving
Proj (g,b) = (curry' g) . b by WAYBEL24:def 2;
hence Proj (g,b) is directed-sups-preserving by A4, FUNCT_6:def 10; :: thesis: verum

end;

hence uncurry f is directed-sups-preserving Function of [:R,S:],T by WAYBEL24:18; :: thesis: verum