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 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 and
A5: 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, 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:4;
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 4;
A9: 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
A10: f in dom G and
A11: g = G . f by FUNCT_1:def 5;
reconsider f = f as directed-sups-preserving Function of [:R,S:],T by A8, A10, Def4;
g = curry f by A7, A8, 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:4;
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:41;
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:28;
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:17; :: thesis: verum