deffunc H₁( Function) -> set = uncurry $1;
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 )
consider F being ManySortedSet of the carrier of (UPS (R,(UPS (S,T)))) 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 2;
A3: rng F c= the carrier of (UPS ([:R,S:],T))

proof

let g be object ; :: 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 object such that
A4: f in dom F and
A5: g = F . f by FUNCT_1:def 3;
reconsider f = f as directed-sups-preserving Function of R,(UPS (S,T)) by A4, Def4;
g = uncurry f by A1, A4, A5;
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:2;
take F ; :: thesis: ( F is uncurrying & F is isomorphic )
thus A6: 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;

deffunc H₂( Function) -> set = curry $1;
consider G being ManySortedSet of the carrier of (UPS ([:R,S:],T)) such that
A7: for f being Element of (UPS ([:R,S:],T)) holds G . f = H₂(f) from PBOOLE:sch 5();
A8: dom G = the carrier of (UPS ([:R,S:],T)) by PARTFUN1:def 2;
A9: rng G c= the carrier of (UPS (R,(UPS (S,T))))

proof

let g be object ; :: 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 object such that
A10: f in dom G and
A11: g = G . f by FUNCT_1:def 3;
reconsider f = f as directed-sups-preserving Function of [:R,S:],T by A10, Def4;
g = curry f by A7, A10, A11;
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 A8, FUNCT_2:2;
UPS (S,T) is full SubRelStr of T |^ the carrier of S by Def4;
then A12: (UPS (S,T)) |^ the carrier of R is full SubRelStr of (T |^ the carrier of S) |^ the carrier of R by YELLOW16:39;
UPS (R,(UPS (S,T))) is full SubRelStr of (UPS (S,T)) |^ the carrier of R by Def4;
then A13: UPS (R,(UPS (S,T))) is non empty full SubRelStr of (T |^ the carrier of S) |^ the carrier of R by A12, YELLOW16:26;
the carrier of [:R,S:] = [: the carrier of R, the carrier of S:] by YELLOW_3:def 2;
then A14: UPS ([:R,S:],T) is non empty full SubRelStr of T |^ [: the carrier of R, the carrier of S:] by Def4;
then A15: F is monotone by A6, A13, Th20;
A16: 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 A7, A8; :: thesis: verum

end;

then A17: G is monotone by A13, A14, 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 the carrier of (UPS (R,(UPS (S,T)))) c= Funcs ( the carrier of R,(Funcs ( the carrier of S, the carrier of T))) by A13, YELLOW_0:def 13;
then A18: G * F = id (UPS (R,(UPS (S,T)))) by A2, A3, A8, A6, A16, Th4;
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 A14, YELLOW_0:def 13;
then F * G = id (UPS ([:R,S:],T)) by A2, A8, A9, A6, A16, Th5;
hence F is isomorphic by A18, A15, A17, YELLOW16:15; :: thesis: verum