let L be complete LATTICE; :: thesis: ( L is continuous implies 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 )

assume A1: L is continuous ; :: thesis: 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

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 )
assume A2: for j being Element of J holds rng (F . j) is directed ; :: thesis:
now :: thesis: for c being Element of L st c << Inf holds
c <= Sup
let c be Element of L; :: thesis: ( c << Inf implies c <= Sup )
assume A3: c << Inf ; :: thesis:
A4: for j being Element of J holds c << Sup
proof end;
ex f being Function st
( f in dom () & ( for j being Element of J ex b being Element of L st
( b = (F . j) . (f . j) & c <= b ) ) )
proof
defpred S1[ object , object ] means ( \$1 in J & \$2 in K . \$1 & ex b being Element of L st
( b = (F . \$1) . \$2 & c <= b ) );
A5: for j being Element of J ex k being Element of K . j st c <= (F . j) . k
proof
let j be Element of J; :: thesis: ex k being Element of K . j st c <= (F . j) . k
A6: Sup <= sup (rng (F . j)) by YELLOW_2:def 5;
( rng (F . j) is non empty directed Subset of L & c << Sup ) by A2, A4;
then consider d being Element of L such that
A7: d in rng (F . j) and
A8: c <= d by ;
consider k being object such that
A9: k in dom (F . j) and
A10: d = (F . j) . k by ;
reconsider k = k as Element of K . j by A9;
take k ; :: thesis: c <= (F . j) . k
thus c <= (F . j) . k by ; :: thesis: verum
end;
A11: for j being object st j in J holds
ex k being object st
( k in union (rng K) & S1[j,k] )
proof
let j be object ; :: thesis: ( j in J implies ex k being object st
( k in union (rng K) & S1[j,k] ) )

assume j in J ; :: thesis: ex k being object st
( k in union (rng K) & S1[j,k] )

then reconsider j9 = j as Element of J ;
consider k being Element of K . j9 such that
A12: c <= (F . j9) . k by A5;
take k ; :: thesis: ( k in union (rng K) & S1[j,k] )
j9 in J ;
then j9 in dom K by PARTFUN1:def 2;
then K . j9 in rng K by FUNCT_1:def 3;
hence k in union (rng K) by TARSKI:def 4; :: thesis: S1[j,k]
thus S1[j,k] by A12; :: thesis: verum
end;
consider f being Function such that
A13: dom f = J and
rng f c= union (rng K) and
A14: for j being object st j in J holds
S1[j,f . j] from
A15: now :: thesis: for x being object st x in dom (doms F) holds
f . x in (doms F) . x
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 A16: x in dom F by FUNCT_6:59;
then reconsider j = x as Element of J ;
(doms F) . x = dom (F . j) by
.= K . j by FUNCT_2:def 1 ;
hence f . x in (doms F) . x by A14; :: thesis: verum
end;
dom f = dom F by
.= dom (doms F) by FUNCT_6:59 ;
then f in product (doms F) by ;
then A17: f in dom () by PARTFUN1:def 2;
for j being Element of J holds
( f . j in K . j & ex b being Element of L st
( b = (F . j) . (f . j) & c <= b ) ) by A14;
hence ex f being Function st
( f in dom () & ( for j being Element of J ex b being Element of L st
( b = (F . j) . (f . j) & c <= b ) ) ) by A17; :: thesis: verum
end;
then consider f being Function such that
A18: f in dom () and
A19: for j being Element of J ex b being Element of L st
( b = (F . j) . (f . j) & c <= b ) ;
reconsider f = f as Element of product (doms F) by A18;
reconsider G = () . f as Function of J, the carrier of L ;
now :: thesis: for j being Element of J holds c <= G . j
let j be Element of J; :: thesis: c <= G . j
j in J ;
then A20: j in dom F by PARTFUN1:def 2;
ex b being Element of L st
( b = (F . j) . (f . j) & c <= b ) by A19;
hence c <= G . j by ; :: thesis: verum
end;
then A21: c <= Inf by YELLOW_2:55;
set a = Inf ;
Inf in rng () by Th14;
then Inf <= sup (rng ()) by YELLOW_2:22;
then Inf <= Sup by YELLOW_2:def 5;
hence c <= Sup by ; :: thesis: verum
end;
then A22: Inf <= Sup by ;
Inf >= Sup by Th16;
hence Inf = Sup by ; :: thesis: verum