let L be complete LATTICE; :: 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
rng () is directed

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
rng () is directed

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
rng () is directed

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

assume that
A2: x in rng () and
A3: y in rng () ; :: thesis: ex z being Element of L st
( z in rng () & x <= z & y <= z )

consider h being object such that
A4: h in dom () and
A5: y = //\ ((() . h),L) by ;
reconsider h = h as Function by A4;
reconsider H = () . h as Function of J, the carrier of L by ;
consider g being object such that
A6: g in dom () and
A7: x = //\ ((() . g),L) by ;
reconsider g = g as Function by A6;
reconsider G = () . g as Function of J, the carrier of L by ;
A8: ex_inf_of rng (() . g),L by YELLOW_0:17;
defpred S1[ object , object ] 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 ) ) ) );
A9: 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 A10: j in dom F by PARTFUN1:def 2;
then A11: g . j in dom (F . j) by ;
j in J ;
then A12: j in dom F by PARTFUN1:def 2;
then G . j = (F . j) . (g . j) by ;
then A13: G . j in rng (F . j) by ;
A14: h . j in dom (F . j) by A4, A10, Th9;
H . j = (F . j) . (h . j) by A4, A12, Th9;
then A15: H . j in rng (F . j) by ;
rng (F . j) is directed Subset of L by A1;
then consider c being Element of L such that
A16: c in rng (F . j) and
A17: ( G . j <= c & H . j <= c ) by ;
consider k being object such that
A18: k in dom (F . j) and
A19: c = (F . j) . k by ;
reconsider k = k as Element of K . j by A18;
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 ; :: thesis: verum
end;
A20: for j being object st j in J holds
ex k being object st
( k in union (rng K) & S1[j,k] )
proof
let j9 be object ; :: thesis: ( j9 in J implies ex k being object st
( k in union (rng K) & S1[j9,k] ) )

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

then reconsider j = j9 as Element of J ;
consider k being Element of K . j such that
A21: ( G . j <= (F . j) . k & H . j <= (F . j) . k ) by A9;
take k ; :: thesis: ( k in union (rng K) & S1[j9,k] )
j in J ;
then j in dom K by PARTFUN1:def 2;
then K . j in rng K by FUNCT_1:def 3;
hence k in union (rng K) by TARSKI:def 4; :: thesis: S1[j9,k]
thus S1[j9,k] by 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 object st j in J holds
S1[j,f . j] from
A24: 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 A25: 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 A23; :: thesis: verum
end;
dom f = dom F by
.= dom (doms F) by FUNCT_6:59 ;
then f in product (doms F) by ;
then A26: f in dom () by PARTFUN1:def 2;
then reconsider Ff = () . f as Function of J, the carrier of L by Th10;
take z = Inf ; :: thesis: ( z in rng () & x <= z & y <= z )
thus z in rng () by ; :: thesis: ( x <= z & y <= z )
A27: x = "/\" ((rng (() . g)),L) by ;
now :: thesis: for j being Element of J holds x <= Ff . j
let j be Element of J; :: thesis: x <= Ff . j
A28: j in J ;
then j in dom G by FUNCT_2:def 1;
then A29: G . j in rng G by FUNCT_1:def 3;
j in dom F by ;
then (F . j) . (f . j) = (() . f) . j by ;
then A30: G . j <= Ff . j by A23;
x is_<=_than rng G by ;
then x <= G . j by A29;
hence x <= Ff . j by ; :: thesis: verum
end;
hence x <= z by YELLOW_2:55; :: thesis: y <= z
A31: ex_inf_of rng (() . h),L by YELLOW_0:17;
A32: y = "/\" ((rng (() . h)),L) by ;
now :: thesis: for j being Element of J holds y <= Ff . j
let j be Element of J; :: thesis: y <= Ff . j
A33: j in J ;
then j in dom H by FUNCT_2:def 1;
then A34: H . j in rng H by FUNCT_1:def 3;
j in dom F by ;
then (F . j) . (f . j) = (() . f) . j by ;
then A35: H . j <= Ff . j by A23;
y is_<=_than rng H by ;
then y <= H . j by A34;
hence y <= Ff . j by ; :: thesis: verum
end;
hence y <= z by YELLOW_2:55; :: thesis: verum
end;
hence rng () is directed by WAYBEL_0:def 1; :: thesis: verum