let L be complete LATTICE; :: thesis:
assume A1: L is continuous ; :: thesis:
let J be non empty set ; :: thesis:
let K be V9() ManySortedSet of ; :: thesis:
let F be DoubleIndexedSet of K,L; :: thesis:
assume A2: for j being Element of J holds rng (F . j) is directed ; :: thesis:

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

let j be Element of J; :: thesis:
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:

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 ) ) )

A5: for j being Element of J ex k being Element of K . j st c <= (F . j) . k

let j be Element of J; :: thesis:
A6: rng (F . j) is non empty directed Subset of L by A2;
A7: c << Sup by A4;
Sup <= sup (rng (F . j)) by YELLOW_2:def 5;
then consider d being Element of L such that
A8: d in rng (F . j) and
A9: c <= d by A6, A7, WAYBEL_3:def 1;
consider k being set such that
A10: k in dom (F . j) and
A11: d = (F . j) . k by A8, FUNCT_1:def 5;
reconsider k = k as Element of K . j by A10;
take k ; :: thesis:
thus c <= (F . j) . k by A9, A11; :: thesis:

end;

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 ) );
A12: for j being set st j in J holds
ex k being set st
( k in union (rng K) & S₁[j,k] )

let j be set ; :: thesis:
assume j in J ; :: thesis:
then reconsider j' = j as Element of J ;
consider k being Element of K . j' such that
A13: c <= (F . j') . k by A5;
take k ; :: thesis:
j' in J ;
then j' in dom K by PARTFUN1:def 4;
then ( k in K . j' & K . j' in rng K ) by FUNCT_1:def 5;
hence k in union (rng K) by TARSKI:def 4; :: thesis:
thus S₁[j,k] by A13; :: thesis:

end;

consider f being Function such that
A14: dom f = J and
rng f c= union (rng K) and
A15: for j being set st j in J holds
S₁[j,f . j] from WELLORD2:sch 1(A12);
A16: 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 A15;
A17: dom f = dom F by A14, PARTFUN1:def 4
.= dom (doms F) by FUNCT_6:89 ;

let x be set ; :: thesis:
assume x in dom (doms F) ; :: thesis:
then A18: 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 A18, FUNCT_6:31
.= K . j by FUNCT_2:def 1 ;
hence f . x in (doms F) . x by A15; :: thesis:

end;

then f in product (doms F) by A17, CARD_3:18;
then f in dom (Frege F) by PARTFUN1:def 4;
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 A16; :: thesis:

end;

then consider f being Function such that
A19: f in dom (Frege F) and
A20: 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 A19, Lm7;
reconsider G = (Frege F) . f as Function of J,the carrier of L ;

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

end;

then A22: 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 A22, YELLOW_0:def 2; :: thesis:

end;

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