let R, S, T be complete LATTICE; for f being directed-sups-preserving Function of R,(UPS (S,T)) holds uncurry f is directed-sups-preserving Function of [:R,S:],T
let f be directed-sups-preserving Function of R,(UPS (S,T)); uncurry f is directed-sups-preserving Function of [:R,S:],T
A1:
f in Funcs ( the carrier of R, the carrier of (UPS (S,T)))
by FUNCT_2:11;
Funcs ( the carrier of R, the carrier of (UPS (S,T))) c= Funcs ( the carrier of R,(Funcs ( the carrier of S, the carrier of T)))
by Th22, FUNCT_5:63;
then
uncurry f in Funcs ([: the carrier of R, the carrier of S:], the carrier of T)
by A1, FUNCT_6:20;
then
uncurry f in Funcs ( the carrier of [:R,S:], the carrier of T)
by YELLOW_3:def 2;
then reconsider g = uncurry f as Function of [:R,S:],T by FUNCT_2:121;
A2:
the carrier of (UPS (S,T)) c= Funcs ( the carrier of S, the carrier of T)
by Th22;
now reconsider ST =
UPS (
S,
T) as non
empty full sups-inheriting SubRelStr of
T |^ the
carrier of
S by Def4, Th26;
let a be
Element of
R;
for b being Element of S holds
( Proj (g,a) is directed-sups-preserving & Proj (g,b) is directed-sups-preserving )let b be
Element of
S;
( Proj (g,a) is directed-sups-preserving & Proj (g,b) is directed-sups-preserving )reconsider f9 =
f as
directed-sups-preserving Function of
R,
ST ;
incl (
ST,
(T |^ the carrier of S)) is
directed-sups-preserving
by WAYBEL21:10;
then A3:
(incl (ST,(T |^ the carrier of S))) * f9 is
directed-sups-preserving
by WAYBEL20:29;
the
carrier of
ST c= the
carrier of
(T |^ the carrier of S)
by YELLOW_0:def 13;
then
incl (
ST,
(T |^ the carrier of S))
= id the
carrier of
ST
by YELLOW_9:def 1;
then
f is
directed-sups-preserving Function of
R,
(T |^ the carrier of S)
by A3, FUNCT_2:23;
then A4:
(commute f) . b is
directed-sups-preserving Function of
R,
T
by Th38;
rng f c= Funcs ( the
carrier of
S, the
carrier of
T)
by A2, XBOOLE_1:1;
then
curry g = f
by FUNCT_5:55;
then
Proj (
g,
a)
= f . a
by WAYBEL24:def 1;
hence
Proj (
g,
a) is
directed-sups-preserving
by Def4;
Proj (g,b) is directed-sups-preserving
Proj (
g,
b)
= (curry' g) . b
by WAYBEL24:def 2;
hence
Proj (
g,
b) is
directed-sups-preserving
by A4, FUNCT_6:def 12;
verum end;
hence
uncurry f is directed-sups-preserving Function of [:R,S:],T
by WAYBEL24:18; verum