let R, S, T be complete LATTICE; for f being directed-sups-preserving Function of [:R,S:],T holds curry f is directed-sups-preserving Function of R,(UPS (S,T))
A1:
[: the carrier of R, the carrier of S:] = the carrier of [:R,S:]
by YELLOW_3:def 2;
let f be directed-sups-preserving Function of [:R,S:],T; curry f is directed-sups-preserving Function of R,(UPS (S,T))
A2:
the carrier of (UPS ([:R,S:],T)) c= Funcs ( the carrier of [:R,S:], the carrier of T)
by Th22;
f in the carrier of (UPS ([:R,S:],T))
by Def4;
then
curry f in Funcs ( the carrier of R,(Funcs ( the carrier of S, the carrier of T)))
by A2, A1, FUNCT_6:10;
then A3:
curry f is Function of the carrier of R,(Funcs ( the carrier of S, the carrier of T))
by FUNCT_2:66;
then A4:
dom (curry f) = the carrier of R
by FUNCT_2:def 1;
rng (curry f) c= the carrier of (UPS (S,T))
then reconsider g = curry f as Function of R,(UPS (S,T)) by A4, FUNCT_2:2;
A7:
UPS (S,T) is full SubRelStr of T |^ the carrier of S
by Def4;
A8:
dom f = the carrier of [:R,S:]
by FUNCT_2:def 1;
g is directed-sups-preserving
proof
let A be
Subset of
R;
WAYBEL_0:def 37 ( A is empty or not A is directed or g preserves_sup_of A )
assume
( not
A is
empty &
A is
directed )
;
g preserves_sup_of A
then reconsider B =
A as non
empty directed Subset of
R ;
reconsider gsA =
g . (sup A) as
Element of
(T |^ the carrier of S) by A7, YELLOW_0:58;
assume
ex_sup_of A,
R
;
WAYBEL_0:def 31 ( ex_sup_of g .: A, UPS (S,T) & "\/" ((g .: A),(UPS (S,T))) = g . ("\/" (A,R)) )
thus
ex_sup_of g .: A,
UPS (
S,
T)
by YELLOW_0:17;
"\/" ((g .: A),(UPS (S,T))) = g . ("\/" (A,R))
A9:
for
s being
Element of
S holds
( the carrier of S --> T) . s is
complete LATTICE
;
the
carrier of
(UPS (S,T)) c= the
carrier of
(T |^ the carrier of S)
by A7, YELLOW_0:def 13;
then
g .: B c= the
carrier of
(T |^ the carrier of S)
;
then reconsider gA =
g .: A as non
empty Subset of
(T |^ the carrier of S) ;
A10:
T |^ the
carrier of
S = product ( the carrier of S --> T)
by YELLOW_1:def 5;
then A11:
dom gsA = the
carrier of
S
by WAYBEL_3:27;
A12:
dom gsA = the
carrier of
S
by A10, WAYBEL_3:27;
A13:
now for x being object st x in the carrier of S holds
(sup gA) . x = gsA . xlet x be
object ;
( x in the carrier of S implies (sup gA) . x = gsA . x )assume
x in the
carrier of
S
;
(sup gA) . x = gsA . xthen reconsider s =
x as
Element of
S ;
reconsider s1 =
{s} as non
empty directed Subset of
S by WAYBEL_0:5;
reconsider As =
[:B,s1:] as non
empty directed Subset of
[:R,S:] ;
A14:
f preserves_sup_of As
by WAYBEL_0:def 37;
A15:
ex_sup_of As,
[:R,S:]
by YELLOW_0:17;
( the carrier of S --> T) . s = T
;
hence (sup gA) . x =
sup (pi (gA,s))
by A9, A10, WAYBEL_3:32
.=
sup (f .: As)
by A8, Th9
.=
f . (sup As)
by A14, A15
.=
f . [(sup (proj1 As)),(sup (proj2 As))]
by YELLOW_3:46
.=
f . [(sup A),(sup (proj2 As))]
by FUNCT_5:9
.=
f . [(sup A),(sup {s})]
by FUNCT_5:9
.=
f . (
(sup A),
s)
by YELLOW_0:39
.=
gsA . x
by A4, A12, FUNCT_5:31
;
verum end;
dom (sup gA) = the
carrier of
S
by A10, WAYBEL_3:27;
then
sup gA = gsA
by A13, A11;
hence
"\/" (
(g .: A),
(UPS (S,T)))
= g . ("\/" (A,R))
by Th27;
verum
end;
hence
curry f is directed-sups-preserving Function of R,(UPS (S,T))
; verum