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 <> {} ) } ;
set k = the Element of K;
{ the Element of 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 object such that
A4: g in dom ((curry H) . j) and
A5: ((curry H) . j) . g = x by FUNCT_1:def 3;
reconsider g = g as Element of Funcs (J,FIK) by A4;
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:111;
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:85;
A9: Z c= K by A6, Th20;
assume Y <> {} ; :: thesis:
then Z <> {} by A8;
then Z in FIK by A7, A9;
then A10: {Z} c= FIK by ZFMISC_1:31;
( dom (J --> Z) = J & rng (J --> Z) = {Z} ) by FUNCOP_1:8;
then reconsider g = J --> Z as Element of Funcs (J,FIK) by A10, FUNCT_2:def 2;
A11: g . j = Z ;
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 3; :: 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 object st j in dom (curry F) holds
\\/ (((curry F) . j),L) = \\/ (((curry H) . j),L)

proof

let j9 be object ; :: thesis:
assume j9 in dom (curry F) ; :: thesis:
then reconsider j = j9 as Element of J ;
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 non-empty 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 object 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 object ; :: 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 non-empty 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 2;
then A22: dom h = dom (curry H) by Th8
.= J by Th20 ;
A23: for x being object st x in dom (doms h) holds
(id J) . x in (doms h) . x

proof

let x be object ; :: thesis:
assume x in dom (doms h) ; :: thesis:
then reconsider j = x as Element of J by A22, FUNCT_6:59;
h . j in (J --> (Funcs (J,FIK))) . j by A21, Lm6;
then h . j in Funcs (J,FIK) ;
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_6:22;
hence (id J) . x in (doms h) . x ; :: thesis:

end;

( dom (id J) = J & dom (doms h) = dom h ) by FUNCT_6:59;
then id J in product (doms h) by A22, A23, CARD_3:9;
then A24: id J in dom (Frege h) by PARTFUN1:def 2;
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 2, 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 ; :: thesis:
h . j in (J --> (Funcs (J,FIK))) . j by A21, Lm6;
hence h . j in Funcs (J,FIK) ; :: 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 3;
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 object st j in J holds
not f9 . j is empty ;
hence (Frege h) . (id J) is non-empty ManySortedSet of J by PBOOLE:def 13; :: thesis:
A30: rng ((Frege h) . (id J)) c= FIK

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng ((Frege h) . (id J)) ; :: thesis:
then consider j being object such that
A31: j in dom ((Frege h) . (id J)) and
A32: y = ((Frege h) . (id J)) . j by FUNCT_1:def 3;
((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;
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₁[ object , object , object ] 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 2;
for x being object st x in dom h holds
h . x is Function

proof

let x be object ; :: 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) ;
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 non-empty ManySortedSet of J by A20;
A36: for j being object st j in J holds
for x being object st x in f . j holds
ex y being object st
( y in (J --> the carrier of L) . j & S₁[y,x,j] )

proof

let i be object ; :: thesis:
assume i in J ; :: thesis:
then reconsider j = i as Element of J ;
let x be object ; :: 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:
thus ( y in (J --> the carrier of L) . i & S₁[y,x,i] ) ; :: thesis:

end;

ex G being ManySortedFunction of f,J --> the carrier of L st
for j being object 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 object 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 object 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 object 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 object st x in f . j holds
(G . j) . x = F . (j,x)

proof

let j be Element of J; :: thesis:
let x be object ; :: 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 object 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 object ; :: according to TARSKI:def 3 :: thesis:
assume y in ((curry F) . j) .: (f . j) ; :: thesis:
then consider x being object 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 6;
reconsider k = x as Element of K by A44;
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 3; :: 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) ;
A49: Inf <= ((Frege (curry H)) . h) . j by YELLOW_2:53;
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:3; :: 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:22;
hence Inf <= sup X by A50, ORDERS_2:3; :: 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 object 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;
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:2; :: thesis:

end;