let L be complete LATTICE; :: thesis:
assume A1: L is continuous ; :: thesis:

hereby :: thesis:

let J, K be non empty set ; :: thesis:
let F be Function of [:J,K:],the carrier of L; :: thesis:
let X be Subset of L; :: thesis:
assume A2: X = { a where a is Element of L : ex f being V9() ManySortedSet of st
( f in Funcs J,(Fin K) & ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . j,x ) & a = Inf ) ) } ; :: thesis:
set FIK = { A where A is Subset of K : ( A is finite & A <> {} ) } ;
consider k being Element of K;
{k} in { A where A is Subset of K : ( A is finite & A <> {} ) } ;
then reconsider FIK = { A where A is Subset of K : ( A is finite & A <> {} ) } as non empty set ;
A3: FIK c= Fin K

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in FIK ; :: thesis:
then consider A being Subset of K such that
A4: ( x = A & A is finite & A <> {} ) ;
thus x in Fin K by A4, FINSUB_1:def 5; :: thesis:

end;

set N = Funcs J,FIK;
deffunc H₁( Element of J, Element of Funcs J,FIK) -> Element of the carrier of L = sup (((curry F) . $1) .: ($2 . $1));
ex H being Function of [:J,(Funcs J,FIK):],the carrier of L st
for j being Element of J
for g being Element of Funcs J,FIK holds H . j,g = H₁(j,g) from BINOP_1:sch 4();
then consider H being Function of [:J,(Funcs J,FIK):],the carrier of L such that
A5: for j being Element of J
for g being Element of Funcs J,FIK holds H . j,g = sup (((curry F) . j) .: (g . j)) ;
set cF = curry F;
set cH = curry H;
A6: for j being Element of J holds
( ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in rng ((curry H) . j) holds
ex Y being finite Subset of (rng ((curry F) . j)) st
( ex_sup_of Y,L & x = "\/" Y,L ) ) & ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds
"\/" Y,L in rng ((curry H) . j) ) )

proof

let j be Element of J; :: thesis:
set D = rng ((curry H) . j);
set R = rng ((curry F) . j);
set Hj = (curry H) . j;
set Fj = (curry F) . j;
thus for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds
ex_sup_of Y,L by YELLOW_0:17; :: thesis:
thus for x being Element of L st x in rng ((curry H) . j) holds
ex Y being finite Subset of (rng ((curry F) . j)) st
( ex_sup_of Y,L & x = "\/" Y,L ) :: thesis:

proof

let x be Element of L; :: thesis:
assume x in rng ((curry H) . j) ; :: thesis:
then consider g being set such that
A7: g in dom ((curry H) . j) and
A8: ((curry H) . j) . g = x by FUNCT_1:def 5;
reconsider g = g as Element of Funcs J,FIK by A7, Th20;
A9: x = H . j,g by A8, Th20
.= sup (((curry F) . j) .: (g . j)) by A5 ;
consider g' being Function such that
A10: g' = g and
A11: dom g' = J and
A12: rng g' c= FIK by FUNCT_2:def 2;
g . j in rng g by A10, A11, FUNCT_1:def 5;
then g . j in FIK by A10, A12;
then consider A being Subset of K such that
A13: ( A = g . j & A is finite & A <> {} ) ;
reconsider Y = ((curry F) . j) .: (g . j) as finite Subset of (rng ((curry F) . j)) by A13, RELAT_1:144;
take Y ; :: thesis:
thus ( ex_sup_of Y,L & x = "\/" Y,L ) by A9, YELLOW_0:17; :: thesis:

end;

thus for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds
"\/" Y,L in rng ((curry H) . j) :: thesis:

proof

let Y be finite Subset of (rng ((curry F) . j)); :: thesis:
assume A14: Y <> {} ; :: thesis:
consider Z being set such that
A15: Z c= dom ((curry F) . j) and
A16: Z is finite and
A17: ((curry F) . j) .: Z = Y by ORDERS_1:195;
A18: Z <> {} by A14, A17, RELAT_1:149;
Z c= K by A15, Th20;
then Z in FIK by A16, A18;
then A19: {Z} c= FIK by ZFMISC_1:37;
A20: dom (J --> Z) = J by FUNCOP_1:19;
rng (J --> Z) = {Z} by FUNCOP_1:14;
then reconsider g = J --> Z as Element of Funcs J,FIK by A19, A20, FUNCT_2:def 2;
g in Funcs J,FIK ;
then A21: g in dom ((curry H) . j) by Th20;
A22: g . j = Z by FUNCOP_1:13;
((curry H) . j) . g = H . j,g by Th20
.= "\/" Y,L by A5, A17, A22 ;
hence "\/" Y,L in rng ((curry H) . j) by A21, FUNCT_1:def 5; :: thesis:

end;

for j being Element of J holds rng ((curry H) . j) is directed

proof

let j be Element of J; :: thesis:
( ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in rng ((curry H) . j) holds
ex Y being finite Subset of (rng ((curry F) . j)) st
( ex_sup_of Y,L & x = "\/" Y,L ) ) & ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds
"\/" Y,L in rng ((curry H) . j) ) ) by A6;
hence rng ((curry H) . j) is directed by WAYBEL_0:51; :: thesis:

end;

then A23: Inf = Sup by A1, Lm8;
A24: dom (curry F) = J by Th20
.= dom (curry H) by Th20 ;
for j being set st j in dom (curry F) holds
\\/ ((curry F) . j),L = \\/ ((curry H) . j),L

proof

let j' be set ; :: thesis:
assume j' in dom (curry F) ; :: thesis:
then reconsider j = j' as Element of J by Th20;
A25: ex_sup_of rng ((curry F) . j),L by YELLOW_0:17;
( ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in rng ((curry H) . j) holds
ex Y being finite Subset of (rng ((curry F) . j)) st
( ex_sup_of Y,L & x = "\/" Y,L ) ) & ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds
"\/" Y,L in rng ((curry H) . j) ) ) by A6;
then sup (rng ((curry F) . j)) = sup (rng ((curry H) . j)) by A25, WAYBEL_0:54;
then Sup = sup (rng ((curry H) . j)) by YELLOW_2:def 5;
hence \\/ ((curry F) . j'),L = \\/ ((curry H) . j'),L by YELLOW_2:def 5; :: thesis:

end;

then A26: Inf = Inf by A24, Th11;
A27: for h being Function-yielding Function st h in product (doms (curry H)) holds
( ( for j being Element of J holds
( ((Frege h) . (id J)) . j = (h . j) . j & h . j in Funcs J,FIK & ((Frege h) . (id J)) . j is non empty finite Subset of K ) ) & (Frege h) . (id J) is V9() ManySortedSet of & (Frege h) . (id J) in Funcs J,FIK & (Frege h) . (id J) in Funcs J,(Fin K) )

proof

let h be Function-yielding Function; :: thesis:
set f = (Frege h) . (id J);
assume h in product (doms (curry H)) ; :: thesis:
then A28: h in dom (Frege (curry H)) by PARTFUN1:def 4;
A29: dom (id J) = J by FUNCT_1:34;
A30: dom (doms h) = dom h by FUNCT_6:89;
A31: dom h = dom (curry H) by A28, Th8
.= J by Th20 ;
for x being set st x in dom (doms h) holds
(id J) . x in (doms h) . x

proof

let x be set ; :: thesis:
assume x in dom (doms h) ; :: thesis:
then reconsider j = x as Element of J by A31, FUNCT_6:89;
A32: (id J) . j = j by FUNCT_1:35;
h . j in (J --> (Funcs J,FIK)) . j by A28, Lm6;
then h . j in Funcs J,FIK by FUNCOP_1:13;
then consider g being Function such that
A33: g = h . j and
A34: dom g = J and
rng g c= FIK by FUNCT_2:def 2;
(doms h) . j = J by A31, A33, A34, FUNCT_6:31;
hence (id J) . x in (doms h) . x by A32; :: thesis:

end;

then id J in product (doms h) by A29, A30, A31, CARD_3:18;
then A35: id J in dom (Frege h) by PARTFUN1:def 4;
thus A36: for j being Element of J holds
( ((Frege h) . (id J)) . j = (h . j) . j & h . j in Funcs J,FIK & ((Frege h) . (id J)) . j is non empty finite Subset of K ) :: thesis:

proof

let j be Element of J; :: thesis:
thus A37: ((Frege h) . (id J)) . j = (h . j) . ((id J) . j) by A31, A35, Th9
.= (h . j) . j by FUNCT_1:35 ; :: thesis:
h . j in (J --> (Funcs J,FIK)) . j by A28, Lm6;
hence h . j in Funcs J,FIK by FUNCOP_1:13; :: thesis:
then consider g being Function such that
A38: g = h . j and
A39: dom g = J and
A40: rng g c= FIK by FUNCT_2:def 2;
((Frege h) . (id J)) . j in rng g by A37, A38, A39, FUNCT_1:def 5;
then ((Frege h) . (id J)) . j in FIK by A40;
then consider A being Subset of K such that
A41: ( ((Frege h) . (id J)) . j = A & A is finite & A <> {} ) ;
thus ((Frege h) . (id J)) . j is non empty finite Subset of K by A41; :: thesis:

end;

A42: dom ((Frege h) . (id J)) = J by A31, A35, Th8;
then reconsider f' = (Frege h) . (id J) as ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
for j being set st j in J holds
not f' . j is empty by A36;
hence (Frege h) . (id J) is V9() ManySortedSet of by PBOOLE:def 16; :: thesis:
A43: rng ((Frege h) . (id J)) c= FIK

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng ((Frege h) . (id J)) ; :: thesis:
then consider j being set such that
A44: j in dom ((Frege h) . (id J)) and
A45: y = ((Frege h) . (id J)) . j by FUNCT_1:def 5;
((Frege h) . (id J)) . j is non empty finite Subset of K by A36, A42, A44;
hence y in FIK by A45; :: thesis:

end;

hence (Frege h) . (id J) in Funcs J,FIK by A42, FUNCT_2:def 2; :: thesis:
rng ((Frege h) . (id J)) c= Fin K by A3, A43, XBOOLE_1:1;
hence (Frege h) . (id J) in Funcs J,(Fin K) by A42, FUNCT_2:def 2; :: thesis:

end;

A46: for h being Element of product (doms (curry H)) holds Inf <= sup X

proof

let h be Element of product (doms (curry H)); :: thesis:
h in product (doms (curry H)) ;
then A47: h in dom (Frege (curry H)) by PARTFUN1:def 4;
for x being set st x in dom h holds
h . x is Function

proof

let x be set ; :: thesis:
assume A48: x in dom h ; :: thesis:
dom h = dom (curry H) by A47, Th8
.= J by Th20 ;
then reconsider j = x as Element of J by A48;
h . j in (J --> (Funcs J,FIK)) . j by A47, Lm6;
then h . j in Funcs J,FIK by FUNCOP_1:13;
then ex f being Function st
( h . j = f & dom f = J & rng f c= FIK ) by FUNCT_2:def 2;
hence h . x is Function ; :: thesis:

end;

then reconsider h' = h as Function-yielding Function by FUNCOP_1:def 6;
reconsider f = (Frege h') . (id J) as V9() ManySortedSet of by A27;
A49: f in Funcs J,(Fin K) by A27;
defpred S₁[ set , set , set ] means $1 = F . $3,$2;
A50: for j being set st j in J holds
for x being set st x in f . j holds
ex y being set st
( y in (J --> the carrier of L) . j & S₁[y,x,j] )

proof

let i be set ; :: thesis:
assume i in J ; :: thesis:
then reconsider j = i as Element of J ;
let x be set ; :: thesis:
assume A51: x in f . i ; :: thesis:
f . j is Subset of K by A27;
then reconsider k = x as Element of K by A51;
take y = F . [j,k]; :: thesis:
y in the carrier of L ;
hence ( y in (J --> the carrier of L) . i & S₁[y,x,i] ) by FUNCOP_1:13; :: thesis:

end;

ex G being ManySortedFunction of f,J --> the carrier of L st
for j being set st j in J holds
ex g being Function of (f . j),((J --> the carrier of L) . j) st
( g = G . j & ( for x being set st x in f . j holds
S₁[g . x,x,j] ) ) from MSSUBFAM:sch 1(A50);
then consider G being ManySortedFunction of f,J --> the carrier of L such that
A52: for j being set st j in J holds
ex g being Function of (f . j),((J --> the carrier of L) . j) st
( g = G . j & ( for x being set st x in f . j holds
g . x = F . j,x ) ) ;
reconsider G = G as DoubleIndexedSet of f,L ;
A53: for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . j,x

proof

let j be Element of J; :: thesis:
let x be set ; :: thesis:
assume A54: x in f . j ; :: thesis:
consider g being Function of (f . j),((J --> the carrier of L) . j) such that
A55: g = G . j and
A56: for x being set st x in f . j holds
g . x = F . j,x by A52;
thus (G . j) . x = F . j,x by A54, A55, A56; :: thesis:

end;

Inf is_<=_than rng (Sups )

proof

let y be Element of L; :: according to LATTICE3:def 8 :: thesis:
assume y in rng (Sups ) ; :: thesis:
then consider j being Element of J such that
A57: y = Sup by Th14;
A58: ( ex_sup_of ((curry F) . j) .: (f . j),L & ex_sup_of rng (G . j),L ) by YELLOW_0:17;
((curry F) . j) .: (f . j) c= rng (G . j)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in ((curry F) . j) .: (f . j) ; :: thesis:
then consider x being set such that
A59: x in dom ((curry F) . j) and
A60: x in f . j and
A61: y = ((curry F) . j) . x by FUNCT_1:def 12;
reconsider k = x as Element of K by A59, Th20;
A62: y = F . j,k by A61, Th20
.= (G . j) . k by A53, A60 ;
k in dom (G . j) by A60, FUNCT_2:def 1;
hence y in rng (G . j) by A62, FUNCT_1:def 5; :: thesis:

end;

then sup (((curry F) . j) .: (f . j)) <= sup (rng (G . j)) by A58, YELLOW_0:34;
then A63: sup (((curry F) . j) .: (f . j)) <= Sup by YELLOW_2:def 5;
j in J ;
then A64: j in dom (curry H) by Th20;
h . j in (J --> (Funcs J,FIK)) . j by A47, Lm6;
then reconsider hj = h . j as Element of Funcs J,FIK by FUNCOP_1:13;
A65: sup (((curry F) . j) .: (f . j)) = sup (((curry F) . j) .: (hj . j)) by A27
.= H . j,hj by A5
.= ((curry H) . j) . (h . j) by Th20
.= ((Frege (curry H)) . h) . j by A47, A64, Th9 ;
Inf <= ((Frege (curry H)) . h) . j by YELLOW_2:55;
hence Inf <= y by A57, A63, A65, ORDERS_2:26; :: thesis:

end;

then Inf <= inf (rng (Sups )) by YELLOW_0:33;
then A66: Inf <= Inf by YELLOW_2:def 6;
Inf in X by A2, A49, A53;
then Inf <= sup X by YELLOW_2:24;
hence Inf <= sup X by A66, ORDERS_2:26; :: thesis:

end;

rng (Infs ) is_<=_than sup X

proof

let x be Element of L; :: according to LATTICE3:def 9 :: thesis:
assume x in rng (Infs ) ; :: thesis:
then consider h being set such that
A67: h in dom (Frege (curry H)) and
A68: x = //\ ((Frege (curry H)) . h),L by Th13;
reconsider h = h as Element of product (doms (curry H)) by A67, PARTFUN1:def 4;
Inf <= sup X by A46;
hence x <= sup X by A68; :: thesis:

end;

then sup (rng (Infs )) <= sup X by YELLOW_0:32;
then A69: Inf <= sup X by A23, A26, YELLOW_2:def 5;
Inf >= sup X by A2, Th22;
hence Inf = sup X by A69, ORDERS_2:25; :: thesis:

end;

thus verum ; :: thesis: