let R, S, T be complete LATTICE; :: thesis: for f being directed-sups-preserving Function of [:R,S:],T holds curry f is directed-sups-preserving Function of R,(UPS (S,T))
A1: [: the carrier of R, the carrier of S:] = the carrier of [:R,S:] by YELLOW_3:def 2;
let f be directed-sups-preserving Function of [:R,S:],T; :: thesis: curry f is directed-sups-preserving Function of R,(UPS (S,T))
A2: the carrier of (UPS ([:R,S:],T)) c= Funcs ( the carrier of [:R,S:], the carrier of T) by Th22;
f in the carrier of (UPS ([:R,S:],T)) by Def4;
then curry f in Funcs ( the carrier of R,(Funcs ( the carrier of S, the carrier of T))) by A2, A1, FUNCT_6:10;
then A3: curry f is Function of the carrier of R,(Funcs ( the carrier of S, the carrier of T)) by FUNCT_2:66;
then A4: dom (curry f) = the carrier of R by FUNCT_2:def 1;
rng (curry f) c= the carrier of (UPS (S,T))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (curry f) or y in the carrier of (UPS (S,T)) )
assume y in rng (curry f) ; :: thesis: y in the carrier of (UPS (S,T))
then consider x being object such that
A5: x in dom (curry f) and
A6: y = (curry f) . x by FUNCT_1:def 3;
reconsider x = x as Element of R by A3, A5, FUNCT_2:def 1;
Proj (f,x) is directed-sups-preserving by WAYBEL24:16;
then y is directed-sups-preserving Function of S,T by A6, WAYBEL24:def 1;
hence y in the carrier of (UPS (S,T)) by Def4; :: thesis: verum

end;

then reconsider g = curry f as Function of R,(UPS (S,T)) by A4, FUNCT_2:2;
A7: UPS (S,T) is full SubRelStr of T |^ the carrier of S by Def4;
A8: dom f = the carrier of [:R,S:] by FUNCT_2:def 1;
g is directed-sups-preserving

proof

let A be Subset of R; :: according to WAYBEL_0:def 37 :: thesis: ( A is empty or not A is directed or g preserves_sup_of A )
assume ( not A is empty & A is directed ) ; :: thesis: g preserves_sup_of A
then reconsider B = A as non empty directed Subset of R ;
reconsider gsA = g . (sup A) as Element of (T |^ the carrier of S) by A7, YELLOW_0:58;
assume ex_sup_of A,R ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of g .: A, UPS (S,T) & "\/" ((g .: A),(UPS (S,T))) = g . ("\/" (A,R)) )
thus ex_sup_of g .: A, UPS (S,T) by YELLOW_0:17; :: thesis: "\/" ((g .: A),(UPS (S,T))) = g . ("\/" (A,R))
A9: for s being Element of S holds ( the carrier of S --> T) . s is complete LATTICE ;
the carrier of (UPS (S,T)) c= the carrier of (T |^ the carrier of S) by A7, YELLOW_0:def 13;
then g .: B c= the carrier of (T |^ the carrier of S) ;
then reconsider gA = g .: A as non empty Subset of (T |^ the carrier of S) ;
A10: T |^ the carrier of S = product ( the carrier of S --> T) by YELLOW_1:def 5;
then A11: dom gsA = the carrier of S by WAYBEL_3:27;
A12: dom gsA = the carrier of S by A10, WAYBEL_3:27;

A13: now :: thesis: for x being object st x in the carrier of S holds
(sup gA) . x = gsA . x

let x be object ; :: thesis: ( x in the carrier of S implies (sup gA) . x = gsA . x )
assume x in the carrier of S ; :: thesis: (sup gA) . x = gsA . x
then reconsider s = x as Element of S ;
reconsider s1 = {s} as non empty directed Subset of S by WAYBEL_0:5;
reconsider As = [:B,s1:] as non empty directed Subset of [:R,S:] ;
A14: f preserves_sup_of As by WAYBEL_0:def 37;
A15: ex_sup_of As,[:R,S:] by YELLOW_0:17;
( the carrier of S --> T) . s = T ;
hence (sup gA) . x = sup (pi (gA,s)) by A9, A10, WAYBEL_3:32
.= sup (f .: As) by A8, Th9
.= f . (sup As) by A14, A15
.= f . [(sup (proj1 As)),(sup (proj2 As))] by YELLOW_3:46
.= f . [(sup A),(sup (proj2 As))] by FUNCT_5:9
.= f . [(sup A),(sup {s})] by FUNCT_5:9
.= f . ((sup A),s) by YELLOW_0:39
.= gsA . x by A4, A12, FUNCT_5:31 ;
:: thesis: verum

end;

dom (sup gA) = the carrier of S by A10, WAYBEL_3:27;
then sup gA = gsA by A13, A11;
hence "\/" ((g .: A),(UPS (S,T))) = g . ("\/" (A,R)) by Th27; :: thesis: verum

end;

hence curry f is directed-sups-preserving Function of R,(UPS (S,T)) ; :: thesis: verum