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