let I be non empty set ; :: thesis: 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; :: thesis: ( ( 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 ) ; :: 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 L9 = product J as non empty up-complete Poset by Th11;

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

_{1}[ 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 ; :: 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 A63: 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: ( not y <= "\/" (D,(product J)) or ex b_{1} being Element of the carrier of (product J) st

( b_{1} in D & x <= b_{1} ) )

assume A64: y <= sup D ; :: thesis: ex b_{1} being Element of the carrier of (product J) st

( b_{1} in D & x <= b_{1} )

A77: ( dom F = K & rng F c= D ) and

A78: for k being object st k in K holds

S_{1}[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 ; :: thesis: ( d in D & x <= d )

thus d in D by A79; :: thesis: x <= d

( 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; :: thesis: ( ( 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 ) ; :: 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 L9 = product J as non empty up-complete Poset by Th11;

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 )

defpred Sfor 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

x . i = Bottom (J . i) )

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

deffunc H_{1}( 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 = H_{1}(i)
from PBOOLE:sch 5();

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)

f +* (y | ({} I)) in X ;

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

X is directed

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

take K = K; :: thesis: 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) ; :: thesis: verum

end;for i being Element of I st not i in K holds

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

x . i = Bottom (J . i)

set K = { i where i is Element of I : x . i <> Bottom (J . i) } ;for i being Element of I st not i in K holds

x . i = Bottom (J . i)

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

thus x . i << y . i :: thesis: verum

end;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: ( not y . i <= "\/" (Di,(J . i)) or ex b_{1} being Element of the carrier of (J . i) st

( b_{1} in Di & x . i <= b_{1} ) )

assume A3: y . i <= sup Di ; :: thesis: ex b_{1} being Element of the carrier of (J . i) st

( b_{1} in Di & x . i <= b_{1} )

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)

A7: y +* (i,di) in D ;

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

D is directed

A16: dom y = I by WAYBEL_3:27;

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 ; :: thesis: ( 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; :: thesis: verum

end;( b

assume A3: y . i <= sup Di ; :: thesis: ex b

( b

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)

proof

then reconsider D = { (y +* (i,z)) where z is Element of (J . i) : z in Di } as Subset of (product J) ;
let a be object ; :: 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) and

z in Di ;

then a is Element of (product J) by A5, A6, WAYBEL_3:27;

hence a in the carrier of (product J) ; :: thesis: verum

end;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) and

z in Di ;

A6: now :: thesis: for j being Element of I holds (y +* (i,z)) . j is Element of (J . j)

dom (y +* (i,z)) = I
by A4, FUNCT_7:30;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:31, FUNCT_7:32;

hence (y +* (i,z)) . j is Element of (J . j) ; :: thesis: verum

end;( i = j or i <> j ) ;

then ( ( (y +* (i,z)) . j = z & i = j ) or (y +* (i,z)) . j = y . j ) by A4, FUNCT_7:31, FUNCT_7:32;

hence (y +* (i,z)) . j is Element of (J . j) ; :: thesis: verum

then a is Element of (product J) by A5, A6, WAYBEL_3:27;

hence a in the carrier of (product J) ; :: thesis: verum

A7: y +* (i,di) in D ;

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

D is directed

proof

then reconsider D = D as non empty directed Subset of (product J) ;
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_{1} being Element of the carrier of (product J) st

( b_{1} in D & z1 <= b_{1} & z2 <= b_{1} ) )

assume z1 in D ; :: thesis: ( not z2 in D or ex b_{1} being Element of the carrier of (product J) st

( b_{1} in D & z1 <= b_{1} & z2 <= b_{1} ) )

then consider a1 being Element of (J . i) such that

A8: z1 = y +* (i,a1) and

A9: a1 in Di ;

assume z2 in D ; :: thesis: ex b_{1} being Element of the carrier of (product J) st

( b_{1} in D & z1 <= b_{1} & z2 <= b_{1} )

then consider a2 being Element of (J . i) such that

A10: z2 = y +* (i,a2) and

A11: a2 in Di ;

consider a being Element of (J . i) such that

A12: a in Di and

A13: a >= a1 and

A14: a >= a2 by A9, A11, WAYBEL_0:def 1;

y +* (i,a) in D by A12;

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 A12; :: thesis: ( z1 <= z & z2 <= z )

A15: dom y = I by WAYBEL_3:27;

end;( b

assume z1 in D ; :: thesis: ( not z2 in D or ex b

( b

then consider a1 being Element of (J . i) such that

A8: z1 = y +* (i,a1) and

A9: a1 in Di ;

assume z2 in D ; :: thesis: ex b

( b

then consider a2 being Element of (J . i) such that

A10: z2 = y +* (i,a2) and

A11: a2 in Di ;

consider a being Element of (J . i) such that

A12: a in Di and

A13: a >= a1 and

A14: a >= a2 by A9, A11, WAYBEL_0:def 1;

y +* (i,a) in D by A12;

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 A12; :: thesis: ( z1 <= z & z2 <= z )

A15: dom y = I by WAYBEL_3:27;

now :: thesis: for j being Element of I holds z . j >= z1 . j

hence
z >= z1
by WAYBEL_3:28; :: thesis: z2 <= zlet 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, A15, FUNCT_7:31, FUNCT_7:32;

hence z . j >= z1 . j by A13, YELLOW_0:def 1; :: thesis: verum

end;( 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, A15, FUNCT_7:31, FUNCT_7:32;

hence z . j >= z1 . j by A13, YELLOW_0:def 1; :: thesis: verum

now :: thesis: for j being Element of I holds z . j >= z2 . j

hence
z2 <= z
by WAYBEL_3:28; :: thesis: verumlet 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 A10, A15, FUNCT_7:31, FUNCT_7:32;

hence z . j >= z2 . j by A14, YELLOW_0:def 1; :: thesis: verum

end;( i = j or i <> j ) ;

then ( ( z . j = a & z2 . j = a2 & i = j ) or ( z . j = y . j & z2 . j = y . j ) ) by A10, A15, FUNCT_7:31, FUNCT_7:32;

hence z . j >= z2 . j by A14, YELLOW_0:def 1; :: thesis: verum

A16: dom y = I by WAYBEL_3:27;

now :: thesis: for j being Element of I holds (sup D) . j >= y . j

then
sup D >= y
by WAYBEL_3:28;A17:
Di c= pi (D,i)

A19: ( 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;

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; :: thesis: verum

end;proof

let j be Element of I; :: thesis: (sup D) . j >= y . j
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Di or a in pi (D,i) )

assume A18: a in Di ; :: thesis: a in pi (D,i)

then reconsider a = a as Element of (J . i) ;

y +* (i,a) in D by A18;

then (y +* (i,a)) . i in pi (D,i) by CARD_3:def 6;

hence a in pi (D,i) by A16, FUNCT_7:31; :: thesis: verum

end;assume A18: a in Di ; :: thesis: a in pi (D,i)

then reconsider a = a as Element of (J . i) ;

y +* (i,a) in D by A18;

then (y +* (i,a)) . i in pi (D,i) by CARD_3:def 6;

hence a in pi (D,i) by A16, FUNCT_7:31; :: thesis: verum

A19: ( 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;

A23: now :: thesis: ( j <> i implies y . j in pi (D,j) )

( not pi (D,j) is empty & pi (D,j) is directed )
by YELLOW16:35;assume
j <> i
; :: thesis: y . j in pi (D,j)

then (y +* (i,di)) . j = y . j by FUNCT_7:32;

hence y . j in pi (D,j) by A7, CARD_3:def 6; :: thesis: verum

end;then (y +* (i,di)) . j = y . j by FUNCT_7:32;

hence y . j in pi (D,j) by A7, CARD_3:def 6; :: thesis: verum

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; :: thesis: verum

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 ; :: thesis: ( 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; :: thesis: verum

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

proof

then reconsider K = { i where i is Element of I : x . i <> Bottom (J . i) } as Subset of I ;
let a be object ; :: 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;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

deffunc H

consider f being ManySortedSet of I such that

A28: for i being Element of I holds f . i = H

A29: now :: thesis: for i being Element of I holds f . i is Element of (J . i)

A30:
dom f = I
by PARTFUN1:def 2;let i be Element of I; :: thesis: f . i is Element of (J . i)

f . i = Bottom (J . i) by A28;

hence f . i is Element of (J . i) ; :: thesis: verum

end;f . i = Bottom (J . i) by A28;

hence f . i is Element of (J . i) ; :: thesis: verum

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)

proof

then reconsider X = { (f +* (y | a)) where a is finite Subset of I : verum } as Subset of (product J) ;
let a be object ; :: 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

A31: a = f +* (y | b) ;

dom y = I by WAYBEL_3:27;

then A32: dom (y | b) = b by RELAT_1:62;

.= dom (f +* (y | b)) by A30, FUNCT_4:def 1 ;

then a is Element of (product J) by A31, A33, WAYBEL_3:27;

hence a in the carrier of (product J) ; :: thesis: verum

end;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

A31: a = f +* (y | b) ;

dom y = I by WAYBEL_3:27;

then A32: dom (y | b) = b by RELAT_1:62;

A33: now :: thesis: for i being Element of I holds (f +* (y | b)) . i is Element of (J . i)

I =
I \/ (dom (y | b))
by A32, XBOOLE_1:12
let i be Element of I; :: thesis: (f +* (y | b)) . i is Element of (J . i)

( (f +* (y | b)) . i = f . i or ( (f +* (y | b)) . i = (y | b) . i & (y | b) . i = y . i ) ) by A32, FUNCT_1:47, FUNCT_4:11, FUNCT_4:13;

hence (f +* (y | b)) . i is Element of (J . i) ; :: thesis: verum

end;( (f +* (y | b)) . i = f . i or ( (f +* (y | b)) . i = (y | b) . i & (y | b) . i = y . i ) ) by A32, FUNCT_1:47, FUNCT_4:11, FUNCT_4:13;

hence (f +* (y | b)) . i is Element of (J . i) ; :: thesis: verum

.= dom (f +* (y | b)) by A30, FUNCT_4:def 1 ;

then a is Element of (product J) by A31, A33, WAYBEL_3:27;

hence a in the carrier of (product J) ; :: thesis: verum

f +* (y | ({} I)) in X ;

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

X is directed

proof

then reconsider X = X as non empty directed Subset of (product J) ;
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_{1} being Element of the carrier of (product J) st

( b_{1} in X & z1 <= b_{1} & z2 <= b_{1} ) )

assume z1 in X ; :: thesis: ( not z2 in X or ex b_{1} being Element of the carrier of (product J) st

( b_{1} in X & z1 <= b_{1} & z2 <= b_{1} ) )

then consider a1 being finite Subset of I such that

A34: z1 = f +* (y | a1) ;

assume z2 in X ; :: thesis: ex b_{1} being Element of the carrier of (product J) st

( b_{1} in X & z1 <= b_{1} & z2 <= b_{1} )

then consider a2 being finite Subset of I such that

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

A36: dom y = I by WAYBEL_3:27;

then A37: dom (y | a) = a by RELAT_1:62;

A38: dom (y | a1) = a1 by A36, RELAT_1:62;

A44: dom (y | a2) = a2 by A36, RELAT_1:62;

end;( b

assume z1 in X ; :: thesis: ( not z2 in X or ex b

( b

then consider a1 being finite Subset of I such that

A34: z1 = f +* (y | a1) ;

assume z2 in X ; :: thesis: ex b

( b

then consider a2 being finite Subset of I such that

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

A36: dom y = I by WAYBEL_3:27;

then A37: dom (y | a) = a by RELAT_1:62;

A38: dom (y | a1) = a1 by A36, RELAT_1:62;

now :: thesis: for i being Element of I holds z . i >= z1 . i

hence
z >= z1
by WAYBEL_3:28; :: thesis: z2 <= zlet i be Element of I; :: thesis: z . b_{1} >= z1 . b_{1}

A39: f . i = Bottom (J . i) by A28;

J . i is non empty lower-bounded up-complete Poset by A1;

then A40: Bottom (J . i) <= y . i by YELLOW_0:44;

end;A39: f . i = Bottom (J . i) by A28;

J . i is non empty lower-bounded up-complete Poset by A1;

then A40: Bottom (J . i) <= y . i by 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;

end;

suppose A41:
( not i in a1 & i in a )
; :: thesis: z . b_{1} >= z1 . b_{1}

then
( z . i = (y | a) . i & (y | a) . i = y . i )
by A37, FUNCT_1:47, FUNCT_4:13;

hence z . i >= z1 . i by A34, A38, A40, A39, A41, FUNCT_4:11; :: thesis: verum

end;hence z . i >= z1 . i by A34, A38, A40, A39, A41, FUNCT_4:11; :: thesis: verum

suppose
( not i in a & not i in a1 )
; :: thesis: z . b_{1} >= z1 . b_{1}

then
( z . i = f . i & z1 . i = f . i )
by A34, A37, A38, FUNCT_4:11;

hence z . i >= z1 . i by YELLOW_0:def 1; :: thesis: verum

end;hence z . i >= z1 . i by YELLOW_0:def 1; :: thesis: verum

suppose A42:
( i in a1 & i in a )
; :: thesis: z . b_{1} >= z1 . b_{1}

then A43:
( z . i = (y | a) . i & (y | a) . i = y . i )
by A37, FUNCT_1:47, FUNCT_4:13;

( z1 . i = (y | a1) . i & (y | a1) . i = y . i ) by A34, A38, A42, FUNCT_1:47, FUNCT_4:13;

hence z . i >= z1 . i by A43, YELLOW_0:def 1; :: thesis: verum

end;( z1 . i = (y | a1) . i & (y | a1) . i = y . i ) by A34, A38, A42, FUNCT_1:47, FUNCT_4:13;

hence z . i >= z1 . i by A43, YELLOW_0:def 1; :: thesis: verum

A44: dom (y | a2) = a2 by A36, RELAT_1:62;

now :: thesis: for i being Element of I holds z . i >= z2 . i

hence
z2 <= z
by WAYBEL_3:28; :: thesis: verumlet i be Element of I; :: thesis: z . b_{1} >= z2 . b_{1}

A45: f . i = Bottom (J . i) by A28;

J . i is non empty lower-bounded up-complete Poset by A1;

then A46: Bottom (J . i) <= y . i by YELLOW_0:44;

end;A45: f . i = Bottom (J . i) by A28;

J . i is non empty lower-bounded up-complete Poset by A1;

then A46: Bottom (J . i) <= y . i by 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;

end;

suppose A47:
( not i in a2 & i in a )
; :: thesis: z . b_{1} >= z2 . b_{1}

then
( z . i = (y | a) . i & (y | a) . i = y . i )
by A37, FUNCT_1:47, FUNCT_4:13;

hence z . i >= z2 . i by A35, A44, A46, A45, A47, FUNCT_4:11; :: thesis: verum

end;hence z . i >= z2 . i by A35, A44, A46, A45, A47, FUNCT_4:11; :: thesis: verum

suppose
( not i in a & not i in a2 )
; :: thesis: z . b_{1} >= z2 . b_{1}

then
( z . i = f . i & z2 . i = f . i )
by A35, A37, A44, FUNCT_4:11;

hence z . i >= z2 . i by YELLOW_0:def 1; :: thesis: verum

end;hence z . i >= z2 . i by YELLOW_0:def 1; :: thesis: verum

suppose A48:
( i in a2 & i in a )
; :: thesis: z . b_{1} >= z2 . b_{1}

then A49:
( z . i = (y | a) . i & (y | a) . i = y . i )
by A37, FUNCT_1:47, FUNCT_4:13;

( z2 . i = (y | a2) . i & (y | a2) . i = y . i ) by A35, A44, A48, FUNCT_1:47, FUNCT_4:13;

hence z . i >= z2 . i by A49, YELLOW_0:def 1; :: thesis: verum

end;( z2 . i = (y | a2) . i & (y | a2) . i = y . i ) by A35, A44, A48, FUNCT_1:47, FUNCT_4:13;

hence z . i >= z2 . i by A49, YELLOW_0:def 1; :: thesis: verum

now :: thesis: for i being Element of I holds (sup X) . i >= y . i

then
y <= sup X
by WAYBEL_3:28;let i be Element of I; :: thesis: (sup X) . i >= y . i

reconsider a = {i} as finite Subset of I by ZFMISC_1:31;

A50: f +* (y | a) in X ;

then reconsider z = f +* (y | a) as Element of (product J) ;

ex_sup_of X,L9 by WAYBEL_0:75;

then sup X is_>=_than X by YELLOW_0:30;

then A51: z <= sup X by A50;

dom y = I by WAYBEL_3:27;

then A52: dom (y | a) = a by RELAT_1:62;

A53: i in a by TARSKI:def 1;

then (y | a) . i = y . i by FUNCT_1:49;

then z . i = y . i by A53, A52, FUNCT_4:13;

hence (sup X) . i >= y . i by A51, WAYBEL_3:28; :: thesis: verum

end;reconsider a = {i} as finite Subset of I by ZFMISC_1:31;

A50: f +* (y | a) in X ;

then reconsider z = f +* (y | a) as Element of (product J) ;

ex_sup_of X,L9 by WAYBEL_0:75;

then sup X is_>=_than X by YELLOW_0:30;

then A51: z <= sup X by A50;

dom y = I by WAYBEL_3:27;

then A52: dom (y | a) = a by RELAT_1:62;

A53: i in a by TARSKI:def 1;

then (y | a) . i = y . i by FUNCT_1:49;

then z . i = y . i by A53, A52, FUNCT_4:13;

hence (sup X) . i >= y . i by A51, WAYBEL_3:28; :: thesis: verum

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

proof

then reconsider K = K as finite Subset of I ;
dom y = I
by WAYBEL_3:27;

then A57: dom (y | a) = a by RELAT_1:62;

let j be object ; :: 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

A58: j = i and

A59: x . i <> Bottom (J . i) ;

J . i is non empty lower-bounded up-complete Poset by A1;

then A60: x . i >= Bottom (J . i) by YELLOW_0:44;

assume not j in a ; :: thesis: contradiction

then A61: d . i = f . i by A56, A58, A57, FUNCT_4:11

.= Bottom (J . i) by A28 ;

x . i <= d . i by A55, WAYBEL_3:28;

hence contradiction by A59, A61, A60, ORDERS_2:2; :: thesis: verum

end;then A57: dom (y | a) = a by RELAT_1:62;

let j be object ; :: 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

A58: j = i and

A59: x . i <> Bottom (J . i) ;

J . i is non empty lower-bounded up-complete Poset by A1;

then A60: x . i >= Bottom (J . i) by YELLOW_0:44;

assume not j in a ; :: thesis: contradiction

then A61: d . i = f . i by A56, A58, A57, FUNCT_4:11

.= Bottom (J . i) by A28 ;

x . i <= d . i by A55, WAYBEL_3:28;

hence contradiction by A59, A61, A60, ORDERS_2:2; :: thesis: verum

take K = K; :: thesis: 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) ; :: thesis: verum

( $1 = i & $2 = z & z . i >= x . i );

assume A62: 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 A63: 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: ( not y <= "\/" (D,(product J)) or ex b

( b

assume A64: y <= sup D ; :: thesis: ex b

( b

A65: now :: thesis: for k being object st k in K holds

ex a being object st

( a in D & S_{1}[k,a] )

consider F being Function such that ex a being object st

( a in D & S

let k be object ; :: thesis: ( k in K implies ex a being object st

( a in D & S_{1}[k,a] ) )

assume k in K ; :: thesis: ex a being object st

( a in D & S_{1}[k,a] )

then reconsider i = k as Element of I ;

A66: pi (D,i) is directed

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; :: thesis: ( a in D & S_{1}[k,a] )

thus a in D by A75; :: thesis: S_{1}[k,a]

thus S_{1}[k,a]
by A74, A75, A76; :: thesis: verum

end;( a in D & S

assume k in K ; :: thesis: ex a being object st

( a in D & S

then reconsider i = k as Element of I ;

A66: pi (D,i) is directed

proof

ex_sup_of D,L9
by WAYBEL_0:75;
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_{1} being Element of the carrier of (J . i) st

( b_{1} in pi (D,i) & a <= b_{1} & b <= b_{1} ) )

assume a in pi (D,i) ; :: thesis: ( not b in pi (D,i) or ex b_{1} being Element of the carrier of (J . i) st

( b_{1} in pi (D,i) & a <= b_{1} & b <= b_{1} ) )

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) ; :: thesis: ex b_{1} being Element of the carrier of (J . i) st

( b_{1} in pi (D,i) & a <= b_{1} & b <= b_{1} )

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 ; :: 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 A68, A70, A71, CARD_3:def 6, WAYBEL_3:28; :: thesis: verum

end;( b

assume a in pi (D,i) ; :: thesis: ( not b in pi (D,i) or ex b

( b

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) ; :: thesis: ex b

( b

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 ; :: 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 A68, A70, A71, CARD_3:def 6, WAYBEL_3:28; :: thesis: verum

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; :: thesis: ( a in D & S

thus a in D by A75; :: thesis: S

thus S

A77: ( dom F = K & rng F c= D ) and

A78: for k being object st k in K holds

S

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 ; :: thesis: ( d in D & x <= d )

thus d in D by A79; :: thesis: x <= d

now :: thesis: for i being Element of I holds d . i >= x . i

hence
x <= d
by WAYBEL_3:28; :: thesis: verumlet i be Element of I; :: thesis: d . b_{1} >= x . b_{1}

A81: J . i is non empty lower-bounded up-complete Poset by A1;

end;A81: J . i is non empty lower-bounded up-complete Poset by A1;

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

end;

suppose A82:
i in K
; :: thesis: d . b_{1} >= x . b_{1}

then consider j being Element of I, z being Element of (product J) such that

A83: i = j and

A84: F . i = z and

A85: z . j >= x . j by A78;

z in Y by A77, A82, A84, FUNCT_1:def 3;

then d >= z by A80;

then d . i >= z . i by WAYBEL_3:28;

hence d . i >= x . i by A81, A83, A85, YELLOW_0:def 2; :: thesis: verum

end;A83: i = j and

A84: F . i = z and

A85: z . j >= x . j by A78;

z in Y by A77, A82, A84, FUNCT_1:def 3;

then d >= z by A80;

then d . i >= z . i by WAYBEL_3:28;

hence d . i >= x . i by A81, A83, A85, YELLOW_0:def 2; :: thesis: verum