let R, S, T be complete LATTICE; :: thesis: ex f being Function of (UPS R,(UPS S,T)),(UPS [:R,S:],T) st
( f is uncurrying & f is isomorphic )
deffunc H₁( Function) -> set = uncurry $1;
consider F being ManySortedSet of such that
A1: for f being Element of (UPS R,(UPS S,T)) holds F . f = H₁(f) from PBOOLE:sch 5();
A2: dom F = the carrier of (UPS R,(UPS S,T)) by PARTFUN1:def 4;
A3: rng F c= the carrier of (UPS [:R,S:],T)

proof

let g be set ; :: according to TARSKI:def 3 :: thesis: ( not g in rng F or g in the carrier of (UPS [:R,S:],T) )
assume g in rng F ; :: thesis: g in the carrier of (UPS [:R,S:],T)
then consider f being set such that
A4: ( f in dom F & g = F . f ) by FUNCT_1:def 5;
reconsider f = f as directed-sups-preserving Function of R,(UPS S,T) by A2, A4, Def4;
g = uncurry f by A1, A2, A4;
then g is directed-sups-preserving Function of [:R,S:],T by Th45;
hence g in the carrier of (UPS [:R,S:],T) by Def4; :: thesis: verum

end;

then reconsider F = F as Function of (UPS R,(UPS S,T)),(UPS [:R,S:],T) by A2, FUNCT_2:4;
deffunc H₂( Function) -> set = curry $1;
consider G being ManySortedSet of such that
A5: for f being Element of (UPS [:R,S:],T) holds G . f = H₂(f) from PBOOLE:sch 5();
A6: dom G = the carrier of (UPS [:R,S:],T) by PARTFUN1:def 4;
A7: rng G c= the carrier of (UPS R,(UPS S,T))

proof

let g be set ; :: according to TARSKI:def 3 :: thesis: ( not g in rng G or g in the carrier of (UPS R,(UPS S,T)) )
assume g in rng G ; :: thesis: g in the carrier of (UPS R,(UPS S,T))
then consider f being set such that
A8: ( f in dom G & g = G . f ) by FUNCT_1:def 5;
reconsider f = f as directed-sups-preserving Function of [:R,S:],T by A6, A8, Def4;
g = curry f by A5, A6, A8;
then g is directed-sups-preserving Function of R,(UPS S,T) by Th46;
hence g in the carrier of (UPS R,(UPS S,T)) by Def4; :: thesis: verum

end;

then reconsider G = G as Function of (UPS [:R,S:],T),(UPS R,(UPS S,T)) by A6, FUNCT_2:4;
take F ; :: thesis: ( F is uncurrying & F is isomorphic )
thus A9: F is uncurrying :: thesis: F is isomorphic

proof

hereby :: according to WAYBEL27:def 1 :: thesis: for f being Function st f in dom F holds
F . f = uncurry f

let x be set ; :: thesis: ( x in dom F implies x is Function-yielding Function )
assume x in dom F ; :: thesis: x is Function-yielding Function
then x is Function of R,(UPS S,T) by Def4;
hence x is Function-yielding Function ; :: thesis: verum

end;

thus for f being Function st f in dom F holds
F . f = uncurry f by A1, A2; :: thesis: verum

end;

A10: G is currying

proof

hereby :: according to WAYBEL27:def 2 :: thesis: for f being Function st f in dom G holds
G . f = curry f

let x be set ; :: thesis: ( x in dom G implies ( x is Function & proj1 x is Relation ) )
assume x in dom G ; :: thesis: ( x is Function & proj1 x is Relation )
then reconsider f = x as Function of [:R,S:],T by Def4;
proj1 f = the carrier of [:R,S:] by FUNCT_2:def 1
.= [:the carrier of R,the carrier of S:] by YELLOW_3:def 2 ;
hence ( x is Function & proj1 x is Relation ) ; :: thesis: verum

end;

thus for f being Function st f in dom G holds
G . f = curry f by A5, A6; :: thesis: verum

end;

UPS S,T is full SubRelStr of T |^ the carrier of S by Def4;
then ( UPS R,(UPS S,T) is full SubRelStr of (UPS S,T) |^ the carrier of R & (UPS S,T) |^ the carrier of R is full SubRelStr of (T |^ the carrier of S) |^ the carrier of R ) by Def4, YELLOW16:41;
then A11: UPS R,(UPS S,T) is non empty full SubRelStr of (T |^ the carrier of S) |^ the carrier of R by YELLOW16:28;
the carrier of [:R,S:] = [:the carrier of R,the carrier of S:] by YELLOW_3:def 2;
then A12: UPS [:R,S:],T is non empty full SubRelStr of T |^ [:the carrier of R,the carrier of S:] by Def4;
then A13: F is monotone by A9, A11, Th20;
A14: G is monotone by A10, A11, A12, Th21;
the carrier of ((T |^ the carrier of S) |^ the carrier of R) = Funcs the carrier of R,the carrier of (T |^ the carrier of S) by YELLOW_1:28
.= Funcs the carrier of R,(Funcs the carrier of S,the carrier of T) by YELLOW_1:28 ;
then A15: the carrier of (UPS R,(UPS S,T)) c= Funcs the carrier of R,(Funcs the carrier of S,the carrier of T) by A11, YELLOW_0:def 13;
the carrier of (T |^ [:the carrier of R,the carrier of S:]) = Funcs [:the carrier of R,the carrier of S:],the carrier of T by YELLOW_1:28;
then the carrier of (UPS [:R,S:],T) c= Funcs [:the carrier of R,the carrier of S:],the carrier of T by A12, YELLOW_0:def 13;
then ( F * G = id (UPS [:R,S:],T) & G * F = id (UPS R,(UPS S,T)) ) by A2, A3, A6, A7, A9, A10, A15, Th4, Th5;
hence F is isomorphic by A13, A14, YELLOW16:17; :: thesis: verum