let L be complete LATTICE; :: thesis: ( L is continuous implies for J, K being non empty set
for F being Function of [:J,K:], the carrier of L
for X being Subset of L st 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 object st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) )
}
holds
Inf = sup X )

assume A1: L is continuous ; :: thesis: for J, K being non empty set
for F being Function of [:J,K:], the carrier of L
for X being Subset of L st 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 object st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) )
}
holds
Inf = sup X

hereby :: thesis: verum
let J, K be non empty set ; :: thesis: for F being Function of [:J,K:], the carrier of L
for X being Subset of L st 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 object st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) )
}
holds
Inf = sup X

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: for X being Subset of L st 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 object st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) )
}
holds
Inf = sup X

let X be Subset of L; :: thesis: ( 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 object st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) )
}
implies Inf = sup X )

set N = Funcs (J,FIK);
deffunc H1( Element of J, Element of Funcs (J,FIK)) -> Element of the carrier of L = sup ((() . \$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) = H1(j,g) from 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 ((() . 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 (() . j)) st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in rng (() . j) holds
ex Y being finite Subset of (rng (() . j)) st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of (rng (() . j)) st Y <> {} holds
"\/" (Y,L) in rng (() . j) ) )
proof
let j be Element of J; :: thesis: ( ( for Y being finite Subset of (rng (() . j)) st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in rng (() . j) holds
ex Y being finite Subset of (rng (() . j)) st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of (rng (() . j)) st Y <> {} holds
"\/" (Y,L) in rng (() . j) ) )

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

thus for x being Element of L st x in rng (() . j) holds
ex Y being finite Subset of (rng (() . j)) st
( ex_sup_of Y,L & x = "\/" (Y,L) ) :: thesis: for Y being finite Subset of (rng (() . j)) st Y <> {} holds
"\/" (Y,L) in rng (() . j)
proof
let x be Element of L; :: thesis: ( x in rng (() . j) implies ex Y being finite Subset of (rng (() . j)) st
( ex_sup_of Y,L & x = "\/" (Y,L) ) )

assume x in rng (() . j) ; :: thesis: ex Y being finite Subset of (rng (() . j)) st
( ex_sup_of Y,L & x = "\/" (Y,L) )

then consider g being object such that
A4: g in dom (() . 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 = (() . j) .: (g . j) as finite Subset of (rng (() . j)) by RELAT_1:111;
take Y ; :: thesis: ( ex_sup_of Y,L & x = "\/" (Y,L) )
x = H . (j,g) by
.= sup ((() . j) .: (g . j)) by A2 ;
hence ( ex_sup_of Y,L & x = "\/" (Y,L) ) by YELLOW_0:17; :: thesis: verum
end;
thus for Y being finite Subset of (rng (() . j)) st Y <> {} holds
"\/" (Y,L) in rng (() . j) :: thesis: verum
proof
let Y be finite Subset of (rng (() . j)); :: thesis: ( Y <> {} implies "\/" (Y,L) in rng (() . j) )
consider Z being set such that
A6: Z c= dom (() . j) and
A7: Z is finite and
A8: ((curry F) . j) .: Z = Y by ORDERS_1:85;
A9: Z c= K by ;
assume Y <> {} ; :: thesis: "\/" (Y,L) in rng (() . j)
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 ;
A11: g . j = Z ;
g in Funcs (J,FIK) ;
then A12: g in dom (() . j) by Th20;
(() . j) . g = H . (j,g) by Th20
.= "\/" (Y,L) by A2, A8, A11 ;
hence "\/" (Y,L) in rng (() . j) by ; :: thesis: verum
end;
end;
for j being Element of J holds rng (() . j) is directed
proof
let j be Element of J; :: thesis: rng (() . j) is directed
A13: for Y being finite Subset of (rng (() . j)) st Y <> {} holds
"\/" (Y,L) in rng (() . j) by A3;
( ( for Y being finite Subset of (rng (() . j)) st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in rng (() . j) holds
ex Y being finite Subset of (rng (() . j)) st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) ) by A3;
hence rng (() . j) is directed by ; :: thesis: verum
end;
then A14: Inf = Sup by ;
A15: for j being object st j in dom () holds
\\/ ((() . j),L) = \\/ ((() . j),L)
proof
let j9 be object ; :: thesis: ( j9 in dom () implies \\/ ((() . j9),L) = \\/ ((() . j9),L) )
assume j9 in dom () ; :: thesis: \\/ ((() . j9),L) = \\/ ((() . j9),L)
then reconsider j = j9 as Element of J ;
A16: ( ( for x being Element of L st x in rng (() . j) holds
ex Y being finite Subset of (rng (() . j)) st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of (rng (() . j)) st Y <> {} holds
"\/" (Y,L) in rng (() . j) ) ) by A3;
( ex_sup_of rng (() . j),L & ( for Y being finite Subset of (rng (() . j)) st Y <> {} holds
ex_sup_of Y,L ) ) by YELLOW_0:17;
then sup (rng (() . j)) = sup (rng (() . j)) by ;
then Sup = sup (rng (() . j)) by YELLOW_2:def 5;
hence \\/ ((() . j9),L) = \\/ ((() . j9),L) by YELLOW_2:def 5; :: thesis: verum
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 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: ( not x in FIK or x in Fin K )
assume x in FIK ; :: thesis: x in Fin K
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: verum
end;
A20: for h being Function-yielding Function st h in product (doms ()) holds
( ( for j being Element of J holds
( (() . (id J)) . j = (h . j) . j & h . j in Funcs (J,FIK) & (() . (id J)) . j is non empty finite Subset of K ) ) & () . (id J) is V9() ManySortedSet of J & () . (id J) in Funcs (J,FIK) & () . (id J) in Funcs (J,(Fin K)) )
proof
let h be Function-yielding Function; :: thesis: ( h in product (doms ()) implies ( ( for j being Element of J holds
( (() . (id J)) . j = (h . j) . j & h . j in Funcs (J,FIK) & (() . (id J)) . j is non empty finite Subset of K ) ) & () . (id J) is V9() ManySortedSet of J & () . (id J) in Funcs (J,FIK) & () . (id J) in Funcs (J,(Fin K)) ) )

set f = () . (id J);
assume h in product (doms ()) ; :: thesis: ( ( for j being Element of J holds
( (() . (id J)) . j = (h . j) . j & h . j in Funcs (J,FIK) & (() . (id J)) . j is non empty finite Subset of K ) ) & () . (id J) is V9() ManySortedSet of J & () . (id J) in Funcs (J,FIK) & () . (id J) in Funcs (J,(Fin K)) )

then A21: h in dom (Frege ()) by PARTFUN1:def 2;
then A22: dom h = dom () 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: ( x in dom (doms h) implies (id J) . x in (doms h) . x )
assume x in dom (doms h) ; :: thesis: (id J) . x in (doms h) . x
then reconsider j = x as Element of J by ;
h . j in (J --> (Funcs (J,FIK))) . j by ;
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 ;
hence (id J) . x in (doms h) . x ; :: thesis: verum
end;
( dom (id J) = J & dom (doms h) = dom h ) by FUNCT_6:59;
then id J in product (doms h) by ;
then A24: id J in dom () by PARTFUN1:def 2;
then A25: dom (() . (id J)) = J by ;
then reconsider f9 = () . (id J) as ManySortedSet of J by ;
thus A26: for j being Element of J holds
( (() . (id J)) . j = (h . j) . j & h . j in Funcs (J,FIK) & (() . (id J)) . j is non empty finite Subset of K ) :: thesis: ( () . (id J) is V9() ManySortedSet of J & () . (id J) in Funcs (J,FIK) & () . (id J) in Funcs (J,(Fin K)) )
proof
let j be Element of J; :: thesis: ( (() . (id J)) . j = (h . j) . j & h . j in Funcs (J,FIK) & (() . (id J)) . j is non empty finite Subset of K )
thus A27: (() . (id J)) . j = (h . j) . ((id J) . j) by
.= (h . j) . j ; :: thesis: ( h . j in Funcs (J,FIK) & (() . (id J)) . j is non empty finite Subset of K )
h . j in (J --> (Funcs (J,FIK))) . j by ;
hence h . j in Funcs (J,FIK) ; :: thesis: (() . (id J)) . j is non empty finite Subset of K
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 ;
then ((Frege h) . (id J)) . j in FIK by A29;
then ex A being Subset of K st
( (() . (id J)) . j = A & A is finite & A <> {} ) ;
hence ((Frege h) . (id J)) . j is non empty finite Subset of K ; :: thesis: verum
end;
then for j being object st j in J holds
not f9 . j is empty ;
hence (Frege h) . (id J) is V9() ManySortedSet of J by PBOOLE:def 13; :: thesis: ( () . (id J) in Funcs (J,FIK) & () . (id J) in Funcs (J,(Fin K)) )
A30: rng (() . (id J)) c= FIK
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (() . (id J)) or y in FIK )
assume y in rng (() . (id J)) ; :: thesis: y in FIK
then consider j being object such that
A31: j in dom (() . (id J)) and
A32: y = (() . (id J)) . j by FUNCT_1:def 3;
((Frege h) . (id J)) . j is non empty finite Subset of K by ;
hence y in FIK by A32; :: thesis: verum
end;
hence (Frege h) . (id J) in Funcs (J,FIK) by ; :: thesis: () . (id J) in Funcs (J,(Fin K))
rng (() . (id J)) c= Fin K by ;
hence (Frege h) . (id J) in Funcs (J,(Fin K)) by ; :: thesis: verum
end;
A33: for h being Element of product (doms ()) holds Inf <= sup X
proof
defpred S1[ object , object , object ] means \$1 = F . (\$3,\$2);
let h be Element of product (doms ()); :: thesis:
h in product (doms ()) ;
then A34: h in dom (Frege ()) by PARTFUN1:def 2;
for x being object st x in dom h holds
h . x is Function
proof
let x be object ; :: thesis: ( x in dom h implies h . x is Function )
assume A35: x in dom h ; :: thesis: h . x is Function
dom h = dom () by
.= J by Th20 ;
then reconsider j = x as Element of J by A35;
h . j in (J --> (Funcs (J,FIK))) . j by ;
then h . j in Funcs (J,FIK) ;
hence h . x is Function ; :: thesis: verum
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 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 & S1[y,x,j] )
proof
let i be object ; :: thesis: ( i in J implies for x being object st x in f . i holds
ex y being object st
( y in (J --> the carrier of L) . i & S1[y,x,i] ) )

assume i in J ; :: thesis: for x being object st x in f . i holds
ex y being object st
( y in (J --> the carrier of L) . i & S1[y,x,i] )

then reconsider j = i as Element of J ;
let x be object ; :: thesis: ( x in f . i implies ex y being object st
( y in (J --> the carrier of L) . i & S1[y,x,i] ) )

assume A37: x in f . i ; :: thesis: ex y being object st
( y in (J --> the carrier of L) . i & S1[y,x,i] )

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 (J --> the carrier of L) . i & S1[y,x,i] )
thus ( y in (J --> the carrier of L) . i & S1[y,x,i] ) ; :: thesis: verum
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
S1[g . x,x,j] ) ) from 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: for x being object st x in f . j holds
(G . j) . x = F . (j,x)

let x be object ; :: thesis: ( x in f . j implies (G . j) . x = F . (j,x) )
assume A40: x in f . j ; :: thesis: (G . j) . x = F . (j,x)
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: verum
end;
Inf is_<=_than rng ()
proof
let y be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not y in rng () or Inf <= y )
assume y in rng () ; :: thesis:
then consider j being Element of J such that
A41: y = Sup by Th14;
j in J ;
then A42: j in dom () by Th20;
A43: ((curry F) . j) .: (f . j) c= rng (G . j)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (() . j) .: (f . j) or y in rng (G . j) )
assume y in (() . j) .: (f . j) ; :: thesis: y in rng (G . j)
then consider x being object such that
A44: x in dom (() . j) and
A45: x in f . j and
A46: y = (() . j) . x by FUNCT_1:def 6;
reconsider k = x as Element of K by A44;
A47: k in dom (G . j) by ;
y = F . (j,k) by
.= (G . j) . k by ;
hence y in rng (G . j) by ; :: thesis: verum
end;
( ex_sup_of (() . j) .: (f . j),L & ex_sup_of rng (G . j),L ) by YELLOW_0:17;
then sup ((() . j) .: (f . j)) <= sup (rng (G . j)) by ;
then A48: sup ((() . j) .: (f . j)) <= Sup by YELLOW_2:def 5;
h . j in (J --> (Funcs (J,FIK))) . j by ;
then reconsider hj = h . j as Element of Funcs (J,FIK) ;
A49: Inf <= ((Frege ()) . h) . j by YELLOW_2:53;
sup ((() . j) .: (f . j)) = sup ((() . j) .: (hj . j)) by A20
.= H . (j,hj) by A2
.= (() . j) . (h . j) by Th20
.= ((Frege ()) . h) . j by ;
hence Inf <= y by ; :: thesis: verum
end;
then Inf <= inf (rng ()) 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 ;
then Inf <= sup X by YELLOW_2:22;
hence Inf <= sup X by ; :: thesis: verum
end;
rng () is_<=_than sup X
proof
let x be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not x in rng () or x <= sup X )
assume x in rng () ; :: thesis: x <= sup X
then consider h being object such that
A51: h in dom (Frege ()) and
A52: x = //\ (((Frege ()) . h),L) by Th13;
reconsider h = h as Element of product (doms ()) by A51;
Inf <= sup X by A33;
hence x <= sup X by A52; :: thesis: verum
end;
then A53: sup (rng ()) <= sup X by YELLOW_0:32;
dom () = J by Th20
.= dom () by Th20 ;
then Inf = Inf by ;
then Inf <= sup X by ;
hence Inf = sup X by ; :: thesis: verum
end;