let I be non empty set ; :: thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of st ( for i being Element of I holds J . i is complete LATTICE ) holds
for x, y being Element of (product J) holds
( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st
for i being Element of I st not i in K holds
x . i = Bottom (J . i) ) )
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of ; :: thesis: ( ( for i being Element of I holds J . i is complete LATTICE ) implies for x, y being Element of (product J) holds
( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st
for i being Element of I st not i in K holds
x . i = Bottom (J . i) ) ) )
set L = product J;
assume A1: for i being Element of I holds J . i is complete LATTICE ; :: thesis: for x, y being Element of (product J) holds
( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st
for i being Element of I st not i in K holds
x . i = Bottom (J . i) ) )
then reconsider L' = product J as complete LATTICE by Th31;
let x, y be Element of (product J); :: thesis: ( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st
for i being Element of I st not i in K holds
x . i = Bottom (J . i) ) )

hereby :: thesis: ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st
for i being Element of I st not i in K holds
x . i = Bottom (J . i) implies x << y )

assume A2: x << y ; :: thesis: ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st
for i being Element of I st not i in K holds
not x . i <> Bottom (J . i) )

hereby :: thesis: ex K being finite Subset of I st
for i being Element of I st not i in K holds
not x . i <> Bottom (J . i)

let i be Element of I; :: thesis: x . i << y . i
thus x . i << y . i :: thesis: verum

proof

let Di be non empty directed Subset of (J . i); :: according to WAYBEL_3:def 1 :: thesis: ( y . i <= sup Di implies ex d being Element of (J . i) st
( d in Di & x . i <= d ) )
assume A3: y . i <= sup Di ; :: thesis: ex d being Element of (J . i) st
( d in Di & x . i <= d )
A4: dom y = I by Th27;
set D = { (y +* i,z) where z is Element of (J . i) : z in Di } ;
{ (y +* i,z) where z is Element of (J . i) : z in Di } c= the carrier of (product J)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (y +* i,z) where z is Element of (J . i) : z in Di } or a in the carrier of (product J) )
assume a in { (y +* i,z) where z is Element of (J . i) : z in Di } ; :: thesis: a in the carrier of (product J)
then consider z being Element of (J . i) such that
A5: ( a = y +* i,z & z in Di ) ;
A6: dom (y +* i,z) = I by A4, FUNCT_7:32;

now

let j be Element of I; :: thesis: (y +* i,z) . j is Element of (J . j)
( i = j or i <> j ) ;
then ( ( (y +* i,z) . j = z & i = j ) or (y +* i,z) . j = y . j ) by A4, FUNCT_7:33, FUNCT_7:34;
hence (y +* i,z) . j is Element of (J . j) ; :: thesis: verum

end;

then a is Element of (product J) by A5, A6, Th27;
hence a in the carrier of (product J) ; :: thesis: verum

end;

then reconsider D = { (y +* i,z) where z is Element of (J . i) : z in Di } as Subset of (product J) ;
consider di being Element of Di;
reconsider di = di as Element of (J . i) ;
A7: ( y +* i,di in D & dom y = I ) by Th27;
then reconsider D = D as non empty Subset of (product J) ;
D is directed

proof

let z1, z2 be Element of (product J); :: according to WAYBEL_0:def 1 :: thesis: ( not z1 in D or not z2 in D or ex b₁ being Element of the carrier of (product J) st
( b₁ in D & z1 <= b₁ & z2 <= b₁ ) )
assume z1 in D ; :: thesis: ( not z2 in D or ex b₁ being Element of the carrier of (product J) st
( b₁ in D & z1 <= b₁ & z2 <= b₁ ) )
then consider a1 being Element of (J . i) such that
A8: ( z1 = y +* i,a1 & a1 in Di ) ;
assume z2 in D ; :: thesis: ex b₁ being Element of the carrier of (product J) st
( b₁ in D & z1 <= b₁ & z2 <= b₁ )
then consider a2 being Element of (J . i) such that
A9: ( z2 = y +* i,a2 & a2 in Di ) ;
consider a being Element of (J . i) such that
A10: ( a in Di & a >= a1 & a >= a2 ) by A8, A9, WAYBEL_0:def 1;
y +* i,a in D by A10;
then reconsider z = y +* i,a as Element of (product J) ;
take z ; :: thesis: ( z in D & z1 <= z & z2 <= z )
thus z in D by A10; :: thesis: ( z1 <= z & z2 <= z )
A11: dom y = I by Th27;

now

let j be Element of I; :: thesis: z . j >= z1 . j
( i = j or i <> j ) ;
then ( ( z . j = a & z1 . j = a1 & i = j ) or ( z . j = y . j & z1 . j = y . j ) ) by A8, A11, FUNCT_7:33, FUNCT_7:34;
hence z . j >= z1 . j by A10, YELLOW_0:def 1; :: thesis: verum

end;

hence z >= z1 by Th28; :: thesis: z2 <= z

now

let j be Element of I; :: thesis: z . j >= z2 . j
( i = j or i <> j ) ;
then ( ( z . j = a & z2 . j = a2 & i = j ) or ( z . j = y . j & z2 . j = y . j ) ) by A9, A11, FUNCT_7:33, FUNCT_7:34;
hence z . j >= z2 . j by A10, YELLOW_0:def 1; :: thesis: verum

end;

hence z2 <= z by Th28; :: thesis: verum

end;

then reconsider D = D as non empty directed Subset of (product J) ;

now

let j be Element of I; :: thesis: (sup D) . j >= y . j
A12: ( J . i is complete LATTICE & J . j is complete LATTICE ) by A1;
then A13: ( ex_sup_of Di,J . i & ex_sup_of pi D,i,J . i ) by YELLOW_0:17;
Di c= pi D,i

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Di or a in pi D,i )
assume A14: a in Di ; :: thesis: a in pi D,i
then reconsider a = a as Element of (J . i) ;
y +* i,a in D by A14;
then (y +* i,a) . i in pi D,i by CARD_3:def 6;
hence a in pi D,i by A7, FUNCT_7:33; :: thesis: verum

end;

then A15: sup Di <= sup (pi D,i) by A13, YELLOW_0:34;
A16: (sup D) . j = sup (pi D,j) by A1, Th32;

now

assume j <> i ; :: thesis: y . j in pi D,j
then ( (y +* i,di) . j = y . j & (y +* i,di) . j in pi D,j ) by A7, CARD_3:def 6, FUNCT_7:34;
hence y . j in pi D,j ; :: thesis: verum

end;

hence (sup D) . j >= y . j by A3, A12, A15, A16, YELLOW_0:def 2, YELLOW_2:24; :: thesis: verum

end;

then sup D >= y by Th28;
then consider d being Element of (product J) such that
A17: ( d in D & d >= x ) by A2, Def1;
consider z being Element of (J . i) such that
A18: ( d = y +* i,z & z in Di ) by A17;
take z ; :: thesis: ( z in Di & x . i <= z )
d . i = z by A4, A18, FUNCT_7:33;
hence ( z in Di & x . i <= z ) by A17, A18, Th28; :: thesis: verum

end;

end;

set K = { i where i is Element of I : x . i <> Bottom (J . i) } ;
{ i where i is Element of I : x . i <> Bottom (J . i) } c= I

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { i where i is Element of I : x . i <> Bottom (J . i) } or a in I )
assume a in { i where i is Element of I : x . i <> Bottom (J . i) } ; :: thesis: a in I
then ex i being Element of I st
( a = i & x . i <> Bottom (J . i) ) ;
hence a in I ; :: thesis: verum

end;

then reconsider K = { i where i is Element of I : x . i <> Bottom (J . i) } as Subset of I ;
deffunc H₁( Element of I) -> Element of the carrier of (J . $1) = Bottom (J . $1);
consider f being ManySortedSet of such that
A19: for i being Element of I holds f . i = H₁(i) from PBOOLE:sch 5();
A20: dom f = I by PARTFUN1:def 4;

now

let i be Element of I; :: thesis: f . i is Element of (J . i)
f . i = Bottom (J . i) by A19;
hence f . i is Element of (J . i) ; :: thesis: verum

end;

then reconsider f = f as Element of (product J) by A20, Th27;
set X = { (f +* (y | a)) where a is finite Subset of I : verum } ;
{ (f +* (y | a)) where a is finite Subset of I : verum } c= the carrier of (product J)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (f +* (y | a)) where a is finite Subset of I : verum } or a in the carrier of (product J) )
assume a in { (f +* (y | a)) where a is finite Subset of I : verum } ; :: thesis: a in the carrier of (product J)
then consider b being finite Subset of I such that
A21: a = f +* (y | b) ;
( dom y = I & b c= I ) by Th27;
then A22: dom (y | b) = b by RELAT_1:91;
then A23: I = I \/ (dom (y | b)) by XBOOLE_1:12
.= dom (f +* (y | b)) by A20, FUNCT_4:def 1 ;

now

let i be Element of I; :: thesis: (f +* (y | b)) . i is Element of (J . i)
( i in b or not i in b ) ;
then ( (f +* (y | b)) . i = f . i or ( (f +* (y | b)) . i = (y | b) . i & (y | b) . i = y . i ) ) by A22, FUNCT_1:70, FUNCT_4:12, FUNCT_4:14;
hence (f +* (y | b)) . i is Element of (J . i) ; :: thesis: verum

end;

then a is Element of (product J) by A21, A23, Th27;
hence a in the carrier of (product J) ; :: thesis: verum

end;

then reconsider X = { (f +* (y | a)) where a is finite Subset of I : verum } as Subset of (product J) ;
f +* (y | ({} I)) in X ;
then reconsider X = X as non empty Subset of (product J) ;
X is directed

proof

let z1, z2 be Element of (product J); :: according to WAYBEL_0:def 1 :: thesis: ( not z1 in X or not z2 in X or ex b₁ being Element of the carrier of (product J) st
( b₁ in X & z1 <= b₁ & z2 <= b₁ ) )
assume z1 in X ; :: thesis: ( not z2 in X or ex b₁ being Element of the carrier of (product J) st
( b₁ in X & z1 <= b₁ & z2 <= b₁ ) )
then consider a1 being finite Subset of I such that
A24: z1 = f +* (y | a1) ;
assume z2 in X ; :: thesis: ex b₁ being Element of the carrier of (product J) st
( b₁ in X & z1 <= b₁ & z2 <= b₁ )
then consider a2 being finite Subset of I such that
A25: z2 = f +* (y | a2) ;
reconsider a = a1 \/ a2 as finite Subset of I ;
f +* (y | a) in X ;
then reconsider z = f +* (y | a) as Element of (product J) ;
take z ; :: thesis: ( z in X & z1 <= z & z2 <= z )
thus z in X ; :: thesis: ( z1 <= z & z2 <= z )
( dom y = I & dom z = I & dom z1 = I & dom z2 = I ) by Th27;
then A26: ( dom (y | a) = a & dom (y | a1) = a1 & dom (y | a2) = a2 ) by RELAT_1:91;

now

let i be Element of I; :: thesis: z . b₁ >= z1 . b₁
J . i is complete LATTICE by A1;
then A27: ( Bottom (J . i) <= y . i & f . i = Bottom (J . i) ) by A19, YELLOW_0:44;

per cases ( ( not i in a1 & i in a ) or ( not i in a & not i in a1 ) or ( i in a1 & i in a ) ) by XBOOLE_0:def 3;

suppose ( not i in a1 & i in a ) ; :: thesis: z . b₁ >= z1 . b₁

then ( z . i = (y | a) . i & (y | a) . i = y . i & z1 . i = f . i ) by A24, A26, FUNCT_1:70, FUNCT_4:12, FUNCT_4:14;
hence z . i >= z1 . i by A27; :: thesis: verum

end;

suppose ( not i in a & not i in a1 ) ; :: thesis: z . b₁ >= z1 . b₁

then ( z . i = f . i & z1 . i = f . i ) by A24, A26, FUNCT_4:12;
hence z . i >= z1 . i by YELLOW_0:def 1; :: thesis: verum

end;

suppose ( i in a1 & i in a ) ; :: thesis: z . b₁ >= z1 . b₁

then ( z . i = (y | a) . i & (y | a) . i = y . i & z1 . i = (y | a1) . i & (y | a1) . i = y . i ) by A24, A26, FUNCT_1:70, FUNCT_4:14;
hence z . i >= z1 . i by YELLOW_0:def 1; :: thesis: verum

end;

end;

end;

hence z >= z1 by Th28; :: thesis: z2 <= z

now

let i be Element of I; :: thesis: z . b₁ >= z2 . b₁
J . i is complete LATTICE by A1;
then A28: ( Bottom (J . i) <= y . i & f . i = Bottom (J . i) ) by A19, YELLOW_0:44;

per cases ( ( not i in a2 & i in a ) or ( not i in a & not i in a2 ) or ( i in a2 & i in a ) ) by XBOOLE_0:def 3;

suppose ( not i in a2 & i in a ) ; :: thesis: z . b₁ >= z2 . b₁

then ( z . i = (y | a) . i & (y | a) . i = y . i & z2 . i = f . i ) by A25, A26, FUNCT_1:70, FUNCT_4:12, FUNCT_4:14;
hence z . i >= z2 . i by A28; :: thesis: verum

end;

suppose ( not i in a & not i in a2 ) ; :: thesis: z . b₁ >= z2 . b₁

then ( z . i = f . i & z2 . i = f . i ) by A25, A26, FUNCT_4:12;
hence z . i >= z2 . i by YELLOW_0:def 1; :: thesis: verum

end;

suppose ( i in a2 & i in a ) ; :: thesis: z . b₁ >= z2 . b₁

then ( z . i = (y | a) . i & (y | a) . i = y . i & z2 . i = (y | a2) . i & (y | a2) . i = y . i ) by A25, A26, FUNCT_1:70, FUNCT_4:14;
hence z . i >= z2 . i by YELLOW_0:def 1; :: thesis: verum

end;

end;

end;

hence z2 <= z by Th28; :: thesis: verum

end;

then reconsider X = X as non empty directed Subset of (product J) ;

now

let i be Element of I; :: thesis: (sup X) . i >= y . i
reconsider a = {i} as finite Subset of I ;
A29: ( f +* (y | a) in X & product J = L' ) ;
then reconsider z = f +* (y | a) as Element of (product J) ;
A30: ( dom y = I & i in a ) by Th27, TARSKI:def 1;
then ( (y | a) . i = y . i & dom (y | a) = a ) by FUNCT_1:72, RELAT_1:91;
then ( z <= sup X & z . i = y . i ) by A29, A30, FUNCT_4:14, YELLOW_2:24;
hence (sup X) . i >= y . i by Th28; :: thesis: verum

end;

then y <= sup X by Th28;
then consider d being Element of (product J) such that
A31: ( d in X & x <= d ) by A2, Def1;
consider a being finite Subset of I such that
A32: d = f +* (y | a) by A31;
K c= a

proof

let j be set ; :: according to TARSKI:def 3 :: thesis: ( not j in K or j in a )
assume j in K ; :: thesis: j in a
then consider i being Element of I such that
A33: ( j = i & x . i <> Bottom (J . i) ) ;
assume A34: not j in a ; :: thesis: contradiction
dom y = I by Th27;
then ( dom (y | a) = a & dom d = I ) by Th27, RELAT_1:91;
then A35: d . i = f . i by A32, A33, A34, FUNCT_4:12
.= Bottom (J . i) by A19 ;
A36: J . i is complete LATTICE by A1;
then ( x . i <= d . i & x . i >= Bottom (J . i) ) by A31, Th28, YELLOW_0:44;
hence contradiction by A33, A35, A36, ORDERS_2:25; :: thesis: verum

end;

then reconsider K = K as finite Subset of I ;
take K = K; :: thesis: for i being Element of I st not i in K holds
not x . i <> Bottom (J . i)
thus for i being Element of I st not i in K holds
not x . i <> Bottom (J . i) ; :: thesis: verum

end;

assume A37: for i being Element of I holds x . i << y . i ; :: thesis: ( for K being finite Subset of I ex i being Element of I st
( not i in K & not x . i = Bottom (J . i) ) or x << y )
given K being finite Subset of I such that A38: for i being Element of I st not i in K holds
x . i = Bottom (J . i) ; :: thesis: x << y
let D be non empty directed Subset of (product J); :: according to WAYBEL_3:def 1 :: thesis: ( y <= sup D implies ex d being Element of (product J) st
( d in D & x <= d ) )
assume A39: y <= sup D ; :: thesis: ex d being Element of (product J) st
( d in D & x <= d )
defpred S₁[ set , set ] means ex i being Element of I ex z being Element of (product J) st
( $1 = i & $2 = z & z . i >= x . i );

A40: now

let k be set ; :: thesis: ( k in K implies ex a being set st
( a in D & S₁[k,a] ) )
assume k in K ; :: thesis: ex a being set st
( a in D & S₁[k,a] )
then reconsider i = k as Element of I ;
A41: pi D,i is directed

proof

let a, b be Element of (J . i); :: according to WAYBEL_0:def 1 :: thesis: ( not a in pi D,i or not b in pi D,i or ex b₁ being Element of the carrier of (J . i) st
( b₁ in pi D,i & a <= b₁ & b <= b₁ ) )
assume a in pi D,i ; :: thesis: ( not b in pi D,i or ex b₁ being Element of the carrier of (J . i) st
( b₁ in pi D,i & a <= b₁ & b <= b₁ ) )
then consider f being Function such that
A42: ( f in D & a = f . i ) by CARD_3:def 6;
assume b in pi D,i ; :: thesis: ex b₁ being Element of the carrier of (J . i) st
( b₁ in pi D,i & a <= b₁ & b <= b₁ )
then consider g being Function such that
A43: ( g in D & b = g . i ) by CARD_3:def 6;
reconsider f = f, g = g as Element of (product J) by A42, A43;
consider h being Element of (product J) such that
A44: ( h in D & h >= f & h >= g ) by A42, A43, WAYBEL_0:def 1;
take h . i ; :: thesis: ( h . i in pi D,i & a <= h . i & b <= h . i )
thus ( h . i in pi D,i & a <= h . i & b <= h . i ) by A42, A43, A44, Th28, CARD_3:def 6; :: thesis: verum

end;

consider dd being Element of D;
reconsider dd = dd as Element of (product J) ;
A45: dd . i in pi D,i by CARD_3:def 6;
( x . i << y . i & y . i <= (sup D) . i & (sup D) . i = sup (pi D,i) ) by A1, A37, A39, Th28, Th32;
then consider zi being Element of (J . i) such that
A46: ( zi in pi D,i & zi >= x . i ) by A41, A45, Def1;
consider a being Function such that
A47: ( a in D & zi = a . i ) by A46, CARD_3:def 6;
reconsider a = a as set ;
take a = a; :: thesis: ( a in D & S₁[k,a] )
thus a in D by A47; :: thesis: S₁[k,a]
thus S₁[k,a] by A46, A47; :: thesis: verum

end;

consider F being Function such that
A48: ( dom F = K & rng F c= D ) and
A49: for k being set st k in K holds
S₁[k,F . k] from WELLORD2:sch 1(A40);
reconsider Y = rng F as finite Subset of D by A48, FINSET_1:26;
product J = L' ;
then consider d being Element of (product J) such that
A50: ( d in D & d is_>=_than Y ) by WAYBEL_0:1;
take d ; :: thesis: ( d in D & x <= d )
thus d in D by A50; :: thesis: x <= d

now

let i be Element of I; :: thesis: d . b₁ >= x . b₁
A51: J . i is complete LATTICE by A1;

per cases ( i in K or not i in K ) ;

suppose A52: i in K ; :: thesis: d . b₁ >= x . b₁

then consider j being Element of I, z being Element of (product J) such that
A53: ( i = j & F . i = z & z . j >= x . j ) by A49;
z in Y by A48, A52, A53, FUNCT_1:def 5;
then d >= z by A50, LATTICE3:def 9;
then d . i >= z . i by Th28;
hence d . i >= x . i by A51, A53, YELLOW_0:def 2; :: thesis: verum

end;

suppose not i in K ; :: thesis: d . b₁ >= x . b₁

then x . i = Bottom (J . i) by A38;
hence d . i >= x . i by A51, YELLOW_0:44; :: thesis: verum

end;

end;

end;

hence x <= d by Th28; :: thesis: verum