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

hereby :: thesis:

let J, K be non empty set ; :: 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 ;
let F be Function of [:J,K:],the carrier of L; :: thesis:
let X be Subset of L; :: thesis:
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
A2: 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;
A3: 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) ) )

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
A4: g in dom ((curry H) . j) and
A5: ((curry H) . j) . g = x by FUNCT_1:def 5;
reconsider g = g as Element of Funcs J,FIK by A4, Th20;
g . j in FIK ;
then ex A being Subset of K st
( A = g . j & A is finite & A <> {} ) ;
then reconsider Y = ((curry F) . j) .: (g . j) as finite Subset of (rng ((curry F) . j)) by RELAT_1:144;
take Y ; :: thesis:
x = H . j,g by A5, Th20
.= sup (((curry F) . j) .: (g . j)) by A2 ;
hence ( ex_sup_of Y,L & x = "\/" Y,L ) by 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:
consider Z being set such that
A6: Z c= dom ((curry F) . j) and
A7: Z is finite and
A8: ((curry F) . j) .: Z = Y by ORDERS_1:195;
A9: Z c= K by A6, Th20;
assume Y <> {} ; :: thesis:
then Z <> {} by A8, RELAT_1:149;
then Z in FIK by A7, A9;
then A10: {Z} c= FIK by ZFMISC_1:37;
( dom (J --> Z) = J & rng (J --> Z) = {Z} ) by FUNCOP_1:14, FUNCOP_1:19;
then reconsider g = J --> Z as Element of Funcs J,FIK by A10, FUNCT_2:def 2;
A11: g . j = Z by FUNCOP_1:13;
g in Funcs J,FIK ;
then A12: g in dom ((curry H) . j) by Th20;
((curry H) . j) . g = H . j,g by Th20
.= "\/" Y,L by A2, A8, A11 ;
hence "\/" Y,L in rng ((curry H) . j) by A12, 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:
A13: for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds
"\/" Y,L in rng ((curry H) . j) by A3;
( ( 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 ) ) ) by A3;
hence rng ((curry H) . j) is directed by A13, WAYBEL_0:51; :: thesis:

end;

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

proof

let j9 be set ; :: thesis:
assume j9 in dom (curry F) ; :: thesis:
then reconsider j = j9 as Element of J by Th20;
A16: ( ( 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 A3;
( ex_sup_of rng ((curry F) . j),L & ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds
ex_sup_of Y,L ) ) by YELLOW_0:17;
then sup (rng ((curry F) . j)) = sup (rng ((curry H) . j)) by A16, WAYBEL_0:54;
then Sup = sup (rng ((curry H) . j)) by YELLOW_2:def 5;
hence \\/ ((curry F) . j9),L = \\/ ((curry H) . j9),L by YELLOW_2:def 5; :: thesis:

end;

assume A17: X = { a where a is Element of L : ex f being V9() ManySortedSet of J 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:
then A18: Inf >= sup X by Th22;
A19: FIK c= Fin K

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in FIK ; :: thesis:
then ex A being Subset of K st
( x = A & A is finite & A <> {} ) ;
hence x in Fin K by FINSUB_1:def 5; :: thesis:

end;

A20: 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 J & (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 A21: h in dom (Frege (curry H)) by PARTFUN1:def 4;
then A22: dom h = dom (curry H) by Th8
.= J by Th20 ;
A23: 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 A22, FUNCT_6:89;
h . j in (J --> (Funcs J,FIK)) . j by A21, Lm6;
then h . j in Funcs J,FIK by FUNCOP_1:13;
then ex g being Function st
( g = h . j & dom g = J & rng g c= FIK ) by FUNCT_2:def 2;
then ( (id J) . j = j & (doms h) . j = J ) by A22, FUNCT_1:35, FUNCT_6:31;
hence (id J) . x in (doms h) . x ; :: thesis:

end;

( dom (id J) = J & dom (doms h) = dom h ) by FUNCT_1:34, FUNCT_6:89;
then id J in product (doms h) by A22, A23, CARD_3:18;
then A24: id J in dom (Frege h) by PARTFUN1:def 4;
then A25: dom ((Frege h) . (id J)) = J by A22, Th8;
then reconsider f9 = (Frege h) . (id J) as ManySortedSet of J by PARTFUN1:def 4, RELAT_1:def 18;
thus A26: 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 A27: ((Frege h) . (id J)) . j = (h . j) . ((id J) . j) by A22, A24, Th9
.= (h . j) . j by FUNCT_1:35 ; :: thesis:
h . j in (J --> (Funcs J,FIK)) . j by A21, Lm6;
hence h . j in Funcs J,FIK by FUNCOP_1:13; :: thesis:
then consider g being Function such that
A28: ( g = h . j & dom g = J ) and
A29: rng g c= FIK by FUNCT_2:def 2;
((Frege h) . (id J)) . j in rng g by A27, A28, FUNCT_1:def 5;
then ((Frege h) . (id J)) . j in FIK by A29;
then ex A being Subset of K st
( ((Frege h) . (id J)) . j = A & A is finite & A <> {} ) ;
hence ((Frege h) . (id J)) . j is non empty finite Subset of K ; :: thesis:

end;

then for j being set st j in J holds
not f9 . j is empty ;
hence (Frege h) . (id J) is V9() ManySortedSet of J by PBOOLE:def 16; :: thesis:
A30: 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
A31: j in dom ((Frege h) . (id J)) and
A32: y = ((Frege h) . (id J)) . j by FUNCT_1:def 5;
((Frege h) . (id J)) . j is non empty finite Subset of K by A26, A25, A31;
hence y in FIK by A32; :: thesis:

end;

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

end;

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

proof

defpred S₁[ set , set , set ] means $1 = F . $3,$2;
let h be Element of product (doms (curry H)); :: thesis:
h in product (doms (curry H)) ;
then A34: 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 A35: x in dom h ; :: thesis:
dom h = dom (curry H) by A34, Th8
.= J by Th20 ;
then reconsider j = x as Element of J by A35;
h . j in (J --> (Funcs J,FIK)) . j by A34, Lm6;
then h . j in Funcs J,FIK by FUNCOP_1:13;
hence h . x is Function ; :: thesis:

end;

then reconsider h9 = h as Function-yielding Function by FUNCOP_1:def 6;
reconsider f = (Frege h9) . (id J) as V9() ManySortedSet of J by A20;
A36: 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 A37: x in f . i ; :: thesis:
f . j is Subset of K by A20;
then reconsider k = x as Element of K by A37;
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(A36);
then consider G being ManySortedFunction of f,J --> the carrier of L such that
A38: 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 ;
A39: 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 A40: x in f . j ; :: thesis:
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 ) ) by A38;
hence (G . j) . x = F . j,x by A40; :: 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
A41: y = Sup by Th14;
j in J ;
then A42: j in dom (curry H) by Th20;
A43: ((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
A44: x in dom ((curry F) . j) and
A45: x in f . j and
A46: y = ((curry F) . j) . x by FUNCT_1:def 12;
reconsider k = x as Element of K by A44, Th20;
A47: k in dom (G . j) by A45, FUNCT_2:def 1;
y = F . j,k by A46, Th20
.= (G . j) . k by A39, A45 ;
hence y in rng (G . j) by A47, FUNCT_1:def 5; :: thesis:

end;

( ex_sup_of ((curry F) . j) .: (f . j),L & ex_sup_of rng (G . j),L ) by YELLOW_0:17;
then sup (((curry F) . j) .: (f . j)) <= sup (rng (G . j)) by A43, YELLOW_0:34;
then A48: sup (((curry F) . j) .: (f . j)) <= Sup by YELLOW_2:def 5;
h . j in (J --> (Funcs J,FIK)) . j by A34, Lm6;
then reconsider hj = h . j as Element of Funcs J,FIK by FUNCOP_1:13;
A49: Inf <= ((Frege (curry H)) . h) . j by YELLOW_2:55;
sup (((curry F) . j) .: (f . j)) = sup (((curry F) . j) .: (hj . j)) by A20
.= H . j,hj by A2
.= ((curry H) . j) . (h . j) by Th20
.= ((Frege (curry H)) . h) . j by A34, A42, Th9 ;
hence Inf <= y by A41, A48, A49, ORDERS_2:26; :: thesis:

end;

then Inf <= inf (rng (Sups )) by YELLOW_0:33;
then A50: Inf <= Inf by YELLOW_2:def 6;
f in Funcs J,(Fin K) by A20;
then Inf in X by A17, A39;
then Inf <= sup X by YELLOW_2:24;
hence Inf <= sup X by A50, 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
A51: h in dom (Frege (curry H)) and
A52: x = //\ ((Frege (curry H)) . h),L by Th13;
reconsider h = h as Element of product (doms (curry H)) by A51, PARTFUN1:def 4;
Inf <= sup X by A33;
hence x <= sup X by A52; :: thesis:

end;

then A53: sup (rng (Infs )) <= sup X by YELLOW_0:32;
dom (curry F) = J by Th20
.= dom (curry H) by Th20 ;
then Inf = Inf by A15, Th11;
then Inf <= sup X by A14, A53, YELLOW_2:def 5;
hence Inf = sup X by A18, ORDERS_2:25; :: thesis:

end;