deffunc H₁( Function) -> set = uncurry $1;
let R, S, T be complete LATTICE; :: thesis:
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))

let g be object ; :: according to TARSKI:def 3 :: thesis:
assume g in rng F ; :: thesis:
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:

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:
thus A6: F is uncurrying :: thesis:

end;

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))))

let g be object ; :: according to TARSKI:def 3 :: thesis:
assume g in rng G ; :: thesis:
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:

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

let x be set ; :: thesis:
assume x in dom G ; :: thesis:
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:

end;

end;