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: Inf = Sup

now

let c be Element of L; :: thesis: ( c << Inf implies c <= Sup )
assume A3: c << Inf ; :: thesis: c <= Sup
A4: for j being Element of J holds c << Sup

proof

let j be Element of J; :: thesis: c << Sup
Sup in rng (Sups ) by Th14;
then inf (rng (Sups )) <= Sup by YELLOW_2:24;
then Inf <= Sup by YELLOW_2:def 6;
hence c << Sup by A3, WAYBEL_3:2; :: thesis: verum

end;

ex f being Function st
( f in dom (Frege F) & ( for j being Element of J ex b being Element of L st
( b = (F . j) . (f . j) & c <= b ) ) )

proof

defpred S₁[ set , set ] 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 A6, WAYBEL_3:def 1;
consider k being set such that
A9: k in dom (F . j) and
A10: d = (F . j) . k by A7, FUNCT_1:def 5;
reconsider k = k as Element of K . j by A9;
take k ; :: thesis: c <= (F . j) . k
thus c <= (F . j) . k by A8, A10; :: thesis: verum

end;

A11: for j being set st j in J holds
ex k being set st
( k in union (rng K) & S₁[j,k] )

proof

let j be set ; :: thesis: ( j in J implies ex k being set st
( k in union (rng K) & S₁[j,k] ) )
assume j in J ; :: thesis: ex k being set st
( k in union (rng K) & S₁[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) & S₁[j,k] )
j9 in J ;
then j9 in dom K by PARTFUN1:def 4;
then K . j9 in rng K by FUNCT_1:def 5;
hence k in union (rng K) by TARSKI:def 4; :: thesis: S₁[j,k]
thus S₁[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 set st j in J holds
S₁[j,f . j] from WELLORD2:sch 1(A11);

A15: now

let x be set ; :: 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:89;
then reconsider j = x as Element of J by PARTFUN1:def 4;
(doms F) . x = dom (F . j) by A16, FUNCT_6:31
.= K . j by FUNCT_2:def 1 ;
hence f . x in (doms F) . x by A14; :: thesis: verum

end;

dom f = dom F by A13, PARTFUN1:def 4
.= dom (doms F) by FUNCT_6:89 ;
then f in product (doms F) by A15, CARD_3:18;
then A17: f in dom (Frege F) by PARTFUN1:def 4;
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 (Frege F) & ( 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 (Frege F) 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, Lm7;
reconsider G = (Frege F) . f as Function of J,the carrier of L ;

now

let j be Element of J; :: thesis: c <= G . j
j in J ;
then A20: j in dom F by PARTFUN1:def 4;
ex b being Element of L st
( b = (F . j) . (f . j) & c <= b ) by A19;
hence c <= G . j by A18, A20, Th9; :: thesis: verum

end;

then A21: c <= Inf by YELLOW_2:57;
set a = Inf ;
Inf in rng (Infs ) by Th14;
then Inf <= sup (rng (Infs )) by YELLOW_2:24;
then Inf <= Sup by YELLOW_2:def 5;
hence c <= Sup by A21, YELLOW_0:def 2; :: thesis: verum

end;

then A22: Inf <= Sup by A1, Th17;
Inf >= Sup by Th16;
hence Inf = Sup by A22, YELLOW_0:def 3; :: thesis: verum