let I be non empty set ; for J being non-Empty Poset-yielding ManySortedSet of I st ( for i being Element of I holds
( J . i is up-complete & J . i is lower-bounded ) ) 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 non-Empty Poset-yielding ManySortedSet of I; ( ( for i being Element of I holds
( J . i is up-complete & J . i is lower-bounded ) ) 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 up-complete & J . i is lower-bounded )
; 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 L9 = product J as non empty up-complete Poset by Th11;
let x, y be Element of (product J); ( 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 ( ( 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
;
( ( 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 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 i be
Element of
I;
x . i << y . ithus
x . i << y . i
verumproof
let Di be non
empty directed Subset of
(J . i);
WAYBEL_3:def 1 ( not y . i <= "\/" (Di,(J . i)) or ex b1 being Element of the carrier of (J . i) st
( b1 in Di & x . i <= b1 ) )
assume A3:
y . i <= sup Di
;
ex b1 being Element of the carrier of (J . i) st
( b1 in Di & x . i <= b1 )
set di = the
Element of
Di;
set D =
{ (y +* (i,z)) where z is Element of (J . i) : z in Di } ;
reconsider di = the
Element of
Di as
Element of
(J . i) ;
A4:
dom y = I
by WAYBEL_3:27;
{ (y +* (i,z)) where z is Element of (J . i) : z in Di } c= the
carrier of
(product J)
then reconsider D =
{ (y +* (i,z)) where z is Element of (J . i) : z in Di } as
Subset of
(product J) ;
A7:
y +* (
i,
di)
in D
;
then reconsider D =
D as non
empty Subset of
(product J) ;
D is
directed
then reconsider D =
D as non
empty directed Subset of
(product J) ;
A16:
dom y = I
by WAYBEL_3:27;
now for j being Element of I holds (sup D) . j >= y . jA17:
Di c= pi (
D,
i)
let j be
Element of
I;
(sup D) . j >= y . jA19:
(
J . i is non
empty up-complete Poset &
J . j is non
empty up-complete Poset )
by A1;
( not
pi (
D,
i) is
empty &
pi (
D,
i) is
directed )
by YELLOW16:35;
then A20:
ex_sup_of pi (
D,
i),
J . i
by A19, WAYBEL_0:75;
ex_sup_of Di,
J . i
by A19, WAYBEL_0:75;
then A21:
sup Di <= sup (pi (D,i))
by A20, A17, YELLOW_0:34;
ex_sup_of D,
L9
by WAYBEL_0:75;
then A22:
(sup D) . j = sup (pi (D,j))
by YELLOW16:33;
( not
pi (
D,
j) is
empty &
pi (
D,
j) is
directed )
by YELLOW16:35;
then
ex_sup_of pi (
D,
j),
J . j
by A19, WAYBEL_0:75;
then
(sup D) . j is_>=_than pi (
D,
j)
by A22, YELLOW_0:30;
hence
(sup D) . j >= y . j
by A3, A21, A22, A23, YELLOW_0:def 2;
verum end;
then
sup D >= y
by WAYBEL_3:28;
then consider d being
Element of
(product J) such that A24:
d in D
and A25:
d >= x
by A2;
consider z being
Element of
(J . i) such that A26:
d = y +* (
i,
z)
and A27:
z in Di
by A24;
take
z
;
( z in Di & x . i <= z )
d . i = z
by A4, A26, FUNCT_7:31;
hence
(
z in Di &
x . i <= z )
by A25, A27, WAYBEL_3:28;
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
then reconsider K =
{ i where i is Element of I : x . i <> Bottom (J . i) } as
Subset of
I ;
deffunc H1(
Element of
I)
-> Element of the
carrier of
(J . $1) =
Bottom (J . $1);
consider f being
ManySortedSet of
I such that A28:
for
i being
Element of
I holds
f . i = H1(
i)
from PBOOLE:sch 5();
A30:
dom f = I
by PARTFUN1:def 2;
then reconsider f =
f as
Element of
(product J) by A29, WAYBEL_3:27;
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)
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
then reconsider X =
X as non
empty directed Subset of
(product J) ;
then
y <= sup X
by WAYBEL_3:28;
then consider d being
Element of
(product J) such that A54:
d in X
and A55:
x <= d
by A2;
consider a being
finite Subset of
I such that A56:
d = f +* (y | a)
by A54;
K c= a
then reconsider K =
K as
finite Subset of
I ;
take K =
K;
for i being Element of I st not i in K holds
x . i = Bottom (J . i)thus
for
i being
Element of
I st not
i in K holds
x . i = Bottom (J . i)
;
verum
end;
defpred S1[ object , object ] means ex i being Element of I ex z being Element of (product J) st
( $1 = i & $2 = z & z . i >= x . i );
assume A62:
for i being Element of I holds x . i << y . i
; ( 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 A63:
for i being Element of I st not i in K holds
x . i = Bottom (J . i)
; x << y
let D be non empty directed Subset of (product J); WAYBEL_3:def 1 ( not y <= "\/" (D,(product J)) or ex b1 being Element of the carrier of (product J) st
( b1 in D & x <= b1 ) )
assume A64:
y <= sup D
; ex b1 being Element of the carrier of (product J) st
( b1 in D & x <= b1 )
A65:
now for k being object st k in K holds
ex a being object st
( a in D & S1[k,a] )let k be
object ;
( k in K implies ex a being object st
( a in D & S1[k,a] ) )assume
k in K
;
ex a being object st
( a in D & S1[k,a] )then reconsider i =
k as
Element of
I ;
A66:
pi (
D,
i) is
directed
proof
let a,
b be
Element of
(J . i);
WAYBEL_0:def 1 ( not a in pi (D,i) or not b in pi (D,i) or ex b1 being Element of the carrier of (J . i) st
( b1 in pi (D,i) & a <= b1 & b <= b1 ) )
assume
a in pi (
D,
i)
;
( not b in pi (D,i) or ex b1 being Element of the carrier of (J . i) st
( b1 in pi (D,i) & a <= b1 & b <= b1 ) )
then consider f being
Function such that A67:
f in D
and A68:
a = f . i
by CARD_3:def 6;
assume
b in pi (
D,
i)
;
ex b1 being Element of the carrier of (J . i) st
( b1 in pi (D,i) & a <= b1 & b <= b1 )
then consider g being
Function such that A69:
g in D
and A70:
b = g . i
by CARD_3:def 6;
reconsider f =
f,
g =
g as
Element of
(product J) by A67, A69;
consider h being
Element of
(product J) such that A71:
(
h in D &
h >= f &
h >= g )
by A67, A69, WAYBEL_0:def 1;
take
h . i
;
( 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 A68, A70, A71, CARD_3:def 6, WAYBEL_3:28;
verum
end;
ex_sup_of D,
L9
by WAYBEL_0:75;
then A72:
(sup D) . i = sup (pi (D,i))
by YELLOW16:33;
(
x . i << y . i &
y . i <= (sup D) . i )
by A62, A64, WAYBEL_3:28;
then consider zi being
Element of
(J . i) such that A73:
zi in pi (
D,
i)
and A74:
zi >= x . i
by A66, A72;
consider a being
Function such that A75:
a in D
and A76:
zi = a . i
by A73, CARD_3:def 6;
reconsider a =
a as
object ;
take a =
a;
( a in D & S1[k,a] )thus
a in D
by A75;
S1[k,a]thus
S1[
k,
a]
by A74, A75, A76;
verum end;
consider F being Function such that
A77:
( dom F = K & rng F c= D )
and
A78:
for k being object st k in K holds
S1[k,F . k]
from FUNCT_1:sch 6(A65);
reconsider Y = rng F as finite Subset of D by A77, FINSET_1:8;
consider d being Element of (product J) such that
A79:
d in D
and
A80:
d is_>=_than Y
by WAYBEL_0:1;
take
d
; ( d in D & x <= d )
thus
d in D
by A79; x <= d
hence
x <= d
by WAYBEL_3:28; verum