let L be complete LATTICE; :: thesis: ( ( for J, K being non empty set
for F being Function of [:J,K:], the carrier of L st ( for j being Element of J holds rng (() . j) is directed ) holds
Inf = Sup ) implies L is continuous )

assume A1: for J, K being non empty set
for F being Function of [:J,K:], the carrier of L st ( for j being Element of J holds rng (() . j) is directed ) holds
Inf = Sup ; :: thesis: L is continuous
for J being non empty set
for K being V9() ManySortedSet of J
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup
proof
let J be non empty set ; :: thesis: for K being V9() ManySortedSet of J
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup

let K be V9() ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup

let F be DoubleIndexedSet of K,L; :: thesis: ( ( for j being Element of J holds rng (F . j) is directed ) implies Inf = Sup )
set j = the Element of J;
set k = the Element of K . the Element of J;
defpred S1[ set , set , set ] means ( \$1 in J & ( ( \$2 in K . \$1 & \$3 = (F . \$1) . \$2 ) or ( not \$2 in K . \$1 & \$3 = Bottom L ) ) );
A2: dom (doms F) = dom F by FUNCT_6:59;
the Element of J in J ;
then the Element of J in dom K by PARTFUN1:def 2;
then ( the Element of K . the Element of J in K . the Element of J & K . the Element of J in rng K ) by FUNCT_1:def 3;
then reconsider K9 = union (rng K) as non empty set by TARSKI:def 4;
A3: dom F = J by PARTFUN1:def 2;
A4: for j being Element of J
for k9 being Element of K9 ex z being Element of L st S1[j,k9,z]
proof
let j be Element of J; :: thesis: for k9 being Element of K9 ex z being Element of L st S1[j,k9,z]
let k9 be Element of K9; :: thesis: ex z being Element of L st S1[j,k9,z]
per cases ( k9 in K . j or not k9 in K . j ) ;
suppose k9 in K . j ; :: thesis: ex z being Element of L st S1[j,k9,z]
then reconsider k = k9 as Element of K . j ;
take (F . j) . k ; :: thesis: S1[j,k9,(F . j) . k]
thus S1[j,k9,(F . j) . k] ; :: thesis: verum
end;
suppose A5: not k9 in K . j ; :: thesis: ex z being Element of L st S1[j,k9,z]
take Bottom L ; :: thesis: S1[j,k9, Bottom L]
thus S1[j,k9, Bottom L] by A5; :: thesis: verum
end;
end;
end;
ex G being Function of [:J,K9:], the carrier of L st
for j being Element of J
for k being Element of K9 holds S1[j,k,G . (j,k)] from then consider G being Function of [:J,K9:], the carrier of L such that
A6: for j being Element of J
for k being Element of K9 holds S1[j,k,G . (j,k)] ;
A7: for j being Element of J holds K . j c= K9
proof
let j be Element of J; :: thesis: K . j c= K9
hereby :: according to TARSKI:def 3 :: thesis: verum
let k be object ; :: thesis: ( k in K . j implies k in K9 )
j in J ;
then j in dom K by PARTFUN1:def 2;
then A8: K . j in rng K by FUNCT_1:def 3;
assume k in K . j ; :: thesis: k in K9
hence k in K9 by ; :: thesis: verum
end;
end;
A9: for j being Element of J holds rng (F . j) c= rng (() . j)
proof
let j be Element of J; :: thesis: rng (F . j) c= rng (() . j)
hereby :: according to TARSKI:def 3 :: thesis: verum
let y be object ; :: thesis: ( y in rng (F . j) implies y in rng (() . j) )
assume y in rng (F . j) ; :: thesis: y in rng (() . j)
then consider k being object such that
A10: k in dom (F . j) and
A11: y = (F . j) . k by FUNCT_1:def 3;
A12: k in K . j by A10;
K . j c= K9 by A7;
then reconsider k = k as Element of K9 by A12;
[j,k] in [:J,K9:] ;
then A13: [j,k] in dom G by FUNCT_2:def 1;
( k in K9 & dom (() . j) = (J --> K9) . j ) by FUNCT_2:def 1;
then A14: k in dom (() . j) ;
y = G . (j,k) by A6, A10, A11
.= (() . j) . k by ;
hence y in rng (() . j) by ; :: thesis: verum
end;
end;
A15: for j being object st j in dom F holds
\\/ ((F . j),L) = \\/ ((() . j),L)
proof
let j9 be object ; :: thesis: ( j9 in dom F implies \\/ ((F . j9),L) = \\/ ((() . j9),L) )
assume j9 in dom F ; :: thesis: \\/ ((F . j9),L) = \\/ ((() . j9),L)
then reconsider j = j9 as Element of J ;
reconsider H = () . j as Function of ((J --> K9) . j), the carrier of L ;
reconsider H = H as Function of K9, the carrier of L ;
for k being Element of K9 holds H . k <= Sup
proof
let k be Element of K9; :: thesis: H . k <= Sup
per cases ( k in K . j or not k in K . j ) ;
suppose A16: k in K . j ; :: thesis: H . k <= Sup
then A17: k in dom (F . j) by FUNCT_2:def 1;
(F . j) . k = G . (j,k) by
.= H . k by Th20 ;
then H . k in rng (F . j) by ;
then H . k <= sup (rng (F . j)) by YELLOW_2:22;
hence H . k <= Sup by YELLOW_2:def 5; :: thesis: verum
end;
suppose not k in K . j ; :: thesis: H . k <= Sup
then Bottom L = G . (j,k) by A6
.= H . k by Th20 ;
hence H . k <= Sup by YELLOW_0:44; :: thesis: verum
end;
end;
end;
then A18: Sup <= Sup by YELLOW_2:54;
( ex_sup_of rng (F . j),L & ex_sup_of rng (() . j),L ) by YELLOW_0:17;
then sup (rng (F . j)) <= sup (rng (() . j)) by ;
then Sup <= sup (rng H) by YELLOW_2:def 5;
then Sup <= Sup by YELLOW_2:def 5;
hence \\/ ((F . j9),L) = \\/ ((() . j9),L) by ; :: thesis: verum
end;
A19: dom (doms ()) = dom () by FUNCT_6:59;
A20: dom () = J by Th20;
product (doms F) c= product (doms ())
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in product (doms F) or x in product (doms ()) )
assume x in product (doms F) ; :: thesis: x in product (doms ())
then consider g being Function such that
A21: x = g and
A22: dom g = dom (doms F) and
A23: for j being object st j in dom (doms F) holds
g . j in (doms F) . j by CARD_3:def 5;
A24: for j being object st j in dom (doms ()) holds
g . j in (doms ()) . j
proof
let j be object ; :: thesis: ( j in dom (doms ()) implies g . j in (doms ()) . j )
assume A25: j in dom (doms ()) ; :: thesis: g . j in (doms ()) . j
then reconsider j9 = j as Element of J by A19;
j in J by ;
then A26: g . j in (doms F) . j by A2, A3, A23;
A27: (doms F) . j = dom (F . j9) by
.= K . j9 by FUNCT_2:def 1 ;
A28: K . j9 c= K9 by A7;
(doms ()) . j = dom (() . j9) by
.= K9 by Th20 ;
hence g . j in (doms ()) . j by ; :: thesis: verum
end;
dom g = dom (doms ()) by A2, A3, A19, A22, Th20;
hence x in product (doms ()) by ; :: thesis: verum
end;
then dom () c= product (doms ()) ;
then A29: dom () c= dom (Frege ()) by PARTFUN1:def 2;
A30: for f being object st f in dom () holds
//\ ((() . f),L) = //\ (((Frege ()) . f),L)
proof
let f9 be object ; :: thesis: ( f9 in dom () implies //\ ((() . f9),L) = //\ (((Frege ()) . f9),L) )
assume A31: f9 in dom () ; :: thesis: //\ ((() . f9),L) = //\ (((Frege ()) . f9),L)
then reconsider f = f9 as Element of product (doms F) ;
A32: dom (() . f) = dom F by
.= J by PARTFUN1:def 2 ;
A33: for j being object st j in J holds
(() . f) . j = ((Frege ()) . f) . j
proof
let j9 be object ; :: thesis: ( j9 in J implies (() . f) . j9 = ((Frege ()) . f) . j9 )
assume j9 in J ; :: thesis: (() . f) . j9 = ((Frege ()) . f) . j9
then reconsider j = j9 as Element of J ;
A34: f . j in K . j by ;
K . j c= K9 by A7;
then reconsider fj = f . j as Element of K9 by A34;
(() . f) . j = (F . j) . fj by
.= G . (j,fj) by
.= (() . j) . (f . j) by Th20
.= ((Frege ()) . f) . j by ;
hence ((Frege F) . f) . j9 = ((Frege ()) . f) . j9 ; :: thesis: verum
end;
dom ((Frege ()) . f) = dom () by
.= proj1 (dom G) by FUNCT_5:def 1
.= proj1 [:J,K9:] by FUNCT_2:def 1
.= J by FUNCT_5:9 ;
hence //\ ((() . f9),L) = //\ (((Frege ()) . f9),L) by ; :: thesis: verum
end;
A35: Sup = Sup
proof
per cases ( for j being Element of J holds K . j = K9 or ex j being Element of J st K . j <> K9 ) ;
suppose A36: for j being Element of J holds K . j = K9 ; :: thesis:
for j being object st j in J holds
(doms F) . j = (doms ()) . j
proof
let j be object ; :: thesis: ( j in J implies (doms F) . j = (doms ()) . j )
assume j in J ; :: thesis: (doms F) . j = (doms ()) . j
then reconsider j9 = j as Element of J ;
A37: (doms F) . j = dom (F . j9) by
.= K . j9 by FUNCT_2:def 1 ;
(doms ()) . j = dom (() . j9) by
.= K9 by Th20 ;
hence (doms F) . j = (doms ()) . j by ; :: thesis: verum
end;
then doms F = doms () by ;
then dom () = product (doms ()) by PARTFUN1:def 2;
then dom () = dom (Frege ()) by PARTFUN1:def 2;
hence Sup = Sup by ; :: thesis: verum
end;
suppose ex j being Element of J st K . j <> K9 ; :: thesis:
then consider j being Element of J such that
A38: K . j <> K9 ;
K . j c= K9 by A7;
then not K9 c= K . j by ;
then consider k being object such that
A39: k in K9 and
A40: not k in K . j ;
reconsider k = k as Element of K9 by A39;
A41: (rng ()) \/ {()} c= rng ()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (rng ()) \/ {()} or x in rng () )
assume A42: x in (rng ()) \/ {()} ; :: thesis: x in rng ()
per cases ( x in rng () or x in {()} ) by ;
suppose x in rng () ; :: thesis: x in rng ()
then consider f being object such that
A43: f in dom () and
A44: x = //\ ((() . f),L) by Th13;
x = //\ (((Frege ()) . f),L) by ;
hence x in rng () by ; :: thesis: verum
end;
suppose A45: x in {()} ; :: thesis: x in rng ()
then reconsider x9 = x as Element of L ;
set f = J --> k;
A46: for x being object st x in dom (doms ()) holds
(J --> k) . x in (doms ()) . x
proof
let x be object ; :: thesis: ( x in dom (doms ()) implies (J --> k) . x in (doms ()) . x )
assume x in dom (doms ()) ; :: thesis: (J --> k) . x in (doms ()) . x
then reconsider j = x as Element of J by A19;
(doms ()) . j = dom (() . j) by
.= K9 by Th20 ;
hence (J --> k) . x in (doms ()) . x ; :: thesis: verum
end;
dom (J --> k) = J
.= dom (doms ()) by ;
then J --> k in product (doms ()) by ;
then A48: J --> k in dom (Frege ()) by PARTFUN1:def 2;
A49: x = Bottom L by ;
then x = G . (j,k) by
.= (() . j) . k by Th20
.= (() . j) . ((J --> k) . j) ;
then x in rng ((Frege ()) . (J --> k)) by ;
then x9 >= "/\" ((rng ((Frege ()) . (J --> k))),L) by YELLOW_2:22;
then A50: x9 >= //\ (((Frege ()) . (J --> k)),L) by YELLOW_2:def 6;
x9 <= //\ (((Frege ()) . (J --> k)),L) by ;
then x9 = //\ (((Frege ()) . (J --> k)),L) by ;
hence x in rng () by ; :: thesis: verum
end;
end;
end;
A51: ( ex_sup_of rng (),L & ex_sup_of {()},L ) by YELLOW_0:17;
A52: rng () c= (rng ()) \/ {()}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng () or x in (rng ()) \/ {()} )
assume x in rng () ; :: thesis: x in (rng ()) \/ {()}
then consider f being object such that
A53: f in dom (Frege ()) and
A54: x = //\ (((Frege ()) . f),L) by Th13;
reconsider f = f as Function by A53;
per cases ( for j being Element of J holds f . j in K . j or ex j being Element of J st not f . j in K . j ) ;
suppose A55: for j being Element of J holds f . j in K . j ; :: thesis: x in (rng ()) \/ {()}
A56: for x being object st x in dom (doms F) holds
f . x in (doms F) . x
proof
let x be object ; :: thesis: ( x in dom (doms F) implies f . x in (doms F) . x )
assume x in dom (doms F) ; :: thesis: f . x in (doms F) . x
then reconsider j = x as Element of J by ;
(doms F) . j = dom (F . j) by
.= K . j by FUNCT_2:def 1 ;
hence f . x in (doms F) . x by A55; :: thesis: verum
end;
dom f = dom () by
.= dom (doms F) by A2, A3, Th20 ;
then f in product (doms F) by ;
then A57: f in dom () by PARTFUN1:def 2;
then x = //\ ((() . f),L) by ;
then x in rng () by ;
hence x in (rng ()) \/ {()} by XBOOLE_0:def 3; :: thesis: verum
end;
suppose not for j being Element of J holds f . j in K . j ; :: thesis: x in (rng ()) \/ {()}
then consider j being Element of J such that
A58: not f . j in K . j ;
j in J ;
then j in dom () by Th20;
then f . j in dom (() . j) by ;
then reconsider k = f . j as Element of K9 ;
Bottom L = G . (j,k) by
.= (() . j) . (f . j) by Th20 ;
then Bottom L in rng ((Frege ()) . f) by ;
then Bottom L >= "/\" ((rng ((Frege ()) . f)),L) by YELLOW_2:22;
then A59: Bottom L >= //\ (((Frege ()) . f),L) by YELLOW_2:def 6;
Bottom L <= //\ (((Frege ()) . f),L) by YELLOW_0:44;
then x = Bottom L by ;
then x in {()} by TARSKI:def 1;
hence x in (rng ()) \/ {()} by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
A60: Bottom L <= Sup by YELLOW_0:44;
Sup = sup (rng ()) by YELLOW_2:def 5
.= sup ((rng ()) \/ {()}) by
.= (sup (rng ())) "\/" (sup {()}) by
.= (sup (rng ())) "\/" () by YELLOW_0:39
.= () "\/" () by YELLOW_2:def 5
.= Sup by ;
hence Sup = Sup ; :: thesis: verum
end;
end;
end;
assume A61: for j being Element of J holds rng (F . j) is directed ; :: thesis:
A62: for j being Element of J holds rng (() . j) is directed
proof
let j be Element of J; :: thesis: rng (() . j) is directed
set X = rng (() . j);
for x, y being Element of L st x in rng (() . j) & y in rng (() . j) holds
ex z being Element of L st
( z in rng (() . j) & x <= z & y <= z )
proof
A63: rng (F . j) is directed by A61;
let x, y be Element of L; :: thesis: ( x in rng (() . j) & y in rng (() . j) implies ex z being Element of L st
( z in rng (() . j) & x <= z & y <= z ) )

assume that
A64: x in rng (() . j) and
A65: y in rng (() . j) ; :: thesis: ex z being Element of L st
( z in rng (() . j) & x <= z & y <= z )

consider b being object such that
A66: b in dom (() . j) and
A67: ((curry G) . j) . b = y by ;
consider a being object such that
A68: a in dom (() . j) and
A69: ((curry G) . j) . a = x by ;
reconsider a9 = a, b9 = b as Element of K9 by ;
A70: x = G . (j,a9) by ;
A71: y = G . (j,b9) by ;
per cases ( ( a in K . j & b in K . j ) or ( a in K . j & not b in K . j ) or ( not a in K . j & b in K . j ) or ( not a in K . j & not b in K . j ) ) ;
suppose A72: ( a in K . j & b in K . j ) ; :: thesis: ex z being Element of L st
( z in rng (() . j) & x <= z & y <= z )

then ( b in dom (F . j) & y = (F . j) . b9 ) by ;
then A73: y in rng (F . j) by FUNCT_1:def 3;
( a in dom (F . j) & x = (F . j) . a9 ) by ;
then x in rng (F . j) by FUNCT_1:def 3;
then consider z being Element of L such that
A74: ( z in rng (F . j) & x <= z & y <= z ) by ;
take z ; :: thesis: ( z in rng (() . j) & x <= z & y <= z )
rng (F . j) c= rng (() . j) by A9;
hence ( z in rng (() . j) & x <= z & y <= z ) by A74; :: thesis: verum
end;
suppose A75: ( a in K . j & not b in K . j ) ; :: thesis: ex z being Element of L st
( z in rng (() . j) & x <= z & y <= z )

take x ; :: thesis: ( x in rng (() . j) & x <= x & y <= x )
y = Bottom L by A6, A71, A75;
hence ( x in rng (() . j) & x <= x & y <= x ) by ; :: thesis: verum
end;
suppose A76: ( not a in K . j & b in K . j ) ; :: thesis: ex z being Element of L st
( z in rng (() . j) & x <= z & y <= z )

take y ; :: thesis: ( y in rng (() . j) & x <= y & y <= y )
x = Bottom L by A6, A70, A76;
hence ( y in rng (() . j) & x <= y & y <= y ) by ; :: thesis: verum
end;
suppose A77: ( not a in K . j & not b in K . j ) ; :: thesis: ex z being Element of L st
( z in rng (() . j) & x <= z & y <= z )

take x ; :: thesis: ( x in rng (() . j) & x <= x & y <= x )
x = Bottom L by A6, A70, A77;
hence ( x in rng (() . j) & x <= x & y <= x ) by A6, A64, A71, A77; :: thesis: verum
end;
end;
end;
hence rng (() . j) is directed by WAYBEL_0:def 1; :: thesis: verum
end;
dom F = J by PARTFUN1:def 2
.= dom () by PARTFUN1:def 2 ;
hence Inf = Inf by
.= Sup by A1, A62, A35 ;
:: thesis: verum
end;
hence L is continuous by Lm9; :: thesis: verum