let L be complete LATTICE; :: thesis: for J being non empty set
for K being V9() ManySortedSet of
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
rng (Infs ) is directed
let J be non empty set ; :: thesis: for K being V9() ManySortedSet of
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
rng (Infs ) is directed
let K be V9() ManySortedSet of ; :: thesis: for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
rng (Infs ) is directed
let F be DoubleIndexedSet of K,L; :: thesis: ( ( for j being Element of J holds rng (F . j) is directed ) implies rng (Infs ) is directed )
assume A1: for j being Element of J holds rng (F . j) is directed ; :: thesis: rng (Infs ) is directed
set X = rng (Infs );
for x, y being Element of L st x in rng (Infs ) & y in rng (Infs ) holds
ex z being Element of L st
( z in rng (Infs ) & x <= z & y <= z )

proof

let x, y be Element of L; :: thesis: ( x in rng (Infs ) & y in rng (Infs ) implies ex z being Element of L st
( z in rng (Infs ) & x <= z & y <= z ) )
assume that
A2: x in rng (Infs ) and
A3: y in rng (Infs ) ; :: thesis: ex z being Element of L st
( z in rng (Infs ) & x <= z & y <= z )
consider g being set such that
A4: g in dom (Frege F) and
A5: x = //\ ((Frege F) . g),L by A2, Th13;
reconsider g = g as Function by A4, Th7;
reconsider G = (Frege F) . g as Function of J,the carrier of L by A4, Th10;
A6: x = "/\" (rng ((Frege F) . g)),L by A5, YELLOW_2:def 6;
A7: ex_inf_of rng ((Frege F) . g),L by YELLOW_0:17;
consider h being set such that
A8: h in dom (Frege F) and
A9: y = //\ ((Frege F) . h),L by A3, Th13;
reconsider h = h as Function by A8, Th7;
reconsider H = (Frege F) . h as Function of J,the carrier of L by A8, Th10;
A10: y = "/\" (rng ((Frege F) . h)),L by A9, YELLOW_2:def 6;
A11: ex_inf_of rng ((Frege F) . h),L by YELLOW_0:17;
A12: for j being Element of J ex k being Element of K . j st
( G . j <= (F . j) . k & H . j <= (F . j) . k )

proof

let j be Element of J; :: thesis: ex k being Element of K . j st
( G . j <= (F . j) . k & H . j <= (F . j) . k )
j in J ;
then j in dom F by PARTFUN1:def 4;
then A13: ( G . j = (F . j) . (g . j) & H . j = (F . j) . (h . j) ) by A4, A8, Th9;
A14: rng (F . j) is directed Subset of L by A1;
j in J ;
then j in dom F by PARTFUN1:def 4;
then ( g . j in dom (F . j) & h . j in dom (F . j) ) by A4, A8, Th9;
then ( G . j in rng (F . j) & H . j in rng (F . j) ) by A13, FUNCT_1:def 5;
then consider c being Element of L such that
A15: c in rng (F . j) and
A16: ( G . j <= c & H . j <= c ) by A14, WAYBEL_0:def 1;
consider k being set such that
A17: k in dom (F . j) and
A18: c = (F . j) . k by A15, FUNCT_1:def 5;
reconsider k = k as Element of K . j by A17;
take k ; :: thesis: ( G . j <= (F . j) . k & H . j <= (F . j) . k )
thus ( G . j <= (F . j) . k & H . j <= (F . j) . k ) by A16, A18; :: thesis: verum

end;

defpred S₁[ set , set ] means ( $1 in J & $2 in K . $1 & ( for c being Element of L st c = (F . $1) . $2 holds
( ( for a being Element of L st a = G . $1 holds
a <= c ) & ( for b being Element of L st b = H . $1 holds
b <= c ) ) ) );
A19: 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 j = j' as Element of J ;
consider k being Element of K . j such that
A20: G . j <= (F . j) . k and
A21: H . j <= (F . j) . k by A12;
take k ; :: thesis: ( k in union (rng K) & S₁[j',k] )
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: S₁[j',k]
thus S₁[j',k] by A20, A21; :: thesis: verum

end;

consider f being Function such that
A22: dom f = J and
rng f c= union (rng K) and
A23: for j being set st j in J holds
S₁[j,f . j] from WELLORD2:sch 1(A19);
A24: dom f = dom F by A22, PARTFUN1:def 4
.= dom (doms F) by FUNCT_6:89 ;

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 A25: 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 A25, FUNCT_6:31
.= K . j by FUNCT_2:def 1 ;
hence f . x in (doms F) . x by A23; :: thesis: verum

end;

then f in product (doms F) by A24, CARD_3:18;
then A26: f in dom (Frege F) by PARTFUN1:def 4;
then reconsider Ff = (Frege F) . f as Function of J,the carrier of L by Th10;
take z = Inf ; :: thesis: ( z in rng (Infs ) & x <= z & y <= z )
thus z in rng (Infs ) by A26, Th13; :: thesis: ( x <= z & y <= z )

now

let j be Element of J; :: thesis: x <= Ff . j
A27: j in J ;
then j in dom G by FUNCT_2:def 1;
then A28: G . j in rng G by FUNCT_1:def 5;
x is_<=_than rng G by A6, A7, YELLOW_0:def 10;
then A29: x <= G . j by A28, LATTICE3:def 8;
j in dom F by A27, PARTFUN1:def 4;
then (F . j) . (f . j) = ((Frege F) . f) . j by A26, Th9;
then G . j <= Ff . j by A23;
hence x <= Ff . j by A29, ORDERS_2:26; :: thesis: verum

end;

hence x <= z by YELLOW_2:57; :: thesis: y <= z

now

let j be Element of J; :: thesis: y <= Ff . j
A30: j in J ;
then j in dom H by FUNCT_2:def 1;
then A31: H . j in rng H by FUNCT_1:def 5;
y is_<=_than rng H by A10, A11, YELLOW_0:def 10;
then A32: y <= H . j by A31, LATTICE3:def 8;
j in dom F by A30, PARTFUN1:def 4;
then (F . j) . (f . j) = ((Frege F) . f) . j by A26, Th9;
then H . j <= Ff . j by A23;
hence y <= Ff . j by A32, ORDERS_2:26; :: thesis: verum

end;

hence y <= z by YELLOW_2:57; :: thesis: verum

end;

hence rng (Infs ) is directed by WAYBEL_0:def 1; :: thesis: verum