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