let L be complete LATTICE; :: thesis: ( ( for J, K being non empty set

for F being Function of [:J,K:], the carrier of L

for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st

( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st

( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds

Inf = sup X ) implies L is continuous )

assume A1: for J, K being non empty set

for F being Function of [:J,K:], the carrier of L

for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st

( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st

( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds

Inf = sup X ; :: thesis: L is continuous

for J, K being non empty set

for F being Function of [:J,K:], the carrier of L st ( for j being Element of J holds rng ((curry F) . j) is directed ) holds

Inf = Sup

for F being Function of [:J,K:], the carrier of L

for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st

( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st

( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds

Inf = sup X ) implies L is continuous )

assume A1: for J, K being non empty set

for F being Function of [:J,K:], the carrier of L

for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st

( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st

( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds

Inf = sup X ; :: thesis: L is continuous

for J, K being non empty set

for F being Function of [:J,K:], the carrier of L st ( for j being Element of J holds rng ((curry F) . j) is directed ) holds

Inf = Sup

proof

hence
L is continuous
by Lm10; :: thesis: verum
let J, K be non empty set ; :: thesis: for F being Function of [:J,K:], the carrier of L st ( for j being Element of J holds rng ((curry F) . j) is directed ) holds

Inf = Sup

let F be Function of [:J,K:], the carrier of L; :: thesis: ( ( for j being Element of J holds rng ((curry F) . j) is directed ) implies Inf = Sup )

assume A2: for j being Element of J holds rng ((curry F) . j) is directed ; :: thesis: Inf = Sup

defpred S_{1}[ Element of L] means ex f being V9() ManySortedSet of J st

( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st

( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) & $1 = Inf ) );

reconsider X = { a where a is Element of L : S_{1}[a] } as Subset of L from DOMAIN_1:sch 7();

X is_<=_than Sup

then A21: Inf <= Sup by A1;

Inf >= Sup by Th16;

hence Inf = Sup by A21, ORDERS_2:2; :: thesis: verum

end;Inf = Sup

let F be Function of [:J,K:], the carrier of L; :: thesis: ( ( for j being Element of J holds rng ((curry F) . j) is directed ) implies Inf = Sup )

assume A2: for j being Element of J holds rng ((curry F) . j) is directed ; :: thesis: Inf = Sup

defpred S

( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st

( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) & $1 = Inf ) );

reconsider X = { a where a is Element of L : S

X is_<=_than Sup

proof

then
sup X <= Sup
by YELLOW_0:32;
let a9 be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a9 in X or a9 <= Sup )

assume a9 in X ; :: thesis: a9 <= Sup

then consider a being Element of L such that

A3: a9 = a and

A4: ex f being V9() ManySortedSet of J st

( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st

( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) & a = Inf ) ) ;

defpred S_{2}[ object , object ] means ( $1 in J & $2 in K & ex b being Element of L st

( b = ((curry F) . $1) . $2 & a <= b ) );

consider f being V9() ManySortedSet of J such that

A5: f in Funcs (J,(Fin K)) and

A6: ex G being DoubleIndexedSet of f,L st

( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) & a = Inf ) by A4;

consider G being DoubleIndexedSet of f,L such that

A7: for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) and

A8: a = Inf by A6;

A9: for x being object st x in J holds

ex y being object st

( y in K & S_{2}[x,y] )

A15: dom g = J and

rng g c= K and

A16: for x being object st x in J holds

S_{2}[x,g . x]
from FUNCT_1:sch 6(A9);

A17: dom (doms (curry F)) = dom (curry F) by FUNCT_6:59;

then A18: dom g = dom (doms (curry F)) by A15, Th20;

for x being object st x in dom (doms (curry F)) holds

g . x in (doms (curry F)) . x

for j being Element of J holds a <= ((Frege (curry F)) . g) . j

Inf in rng (Infs ) by Th14;

then Inf <= sup (rng (Infs )) by YELLOW_2:22;

then Inf <= Sup by YELLOW_2:def 5;

hence a9 <= Sup by A3, A20, ORDERS_2:3; :: thesis: verum

end;assume a9 in X ; :: thesis: a9 <= Sup

then consider a being Element of L such that

A3: a9 = a and

A4: ex f being V9() ManySortedSet of J st

( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st

( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) & a = Inf ) ) ;

defpred S

( b = ((curry F) . $1) . $2 & a <= b ) );

consider f being V9() ManySortedSet of J such that

A5: f in Funcs (J,(Fin K)) and

A6: ex G being DoubleIndexedSet of f,L st

( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) & a = Inf ) by A4;

consider G being DoubleIndexedSet of f,L such that

A7: for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) and

A8: a = Inf by A6;

A9: for x being object st x in J holds

ex y being object st

( y in K & S

proof

consider g being Function such that
let x be object ; :: thesis: ( x in J implies ex y being object st

( y in K & S_{2}[x,y] ) )

assume x in J ; :: thesis: ex y being object st

( y in K & S_{2}[x,y] )

then reconsider j = x as Element of J ;

Sup in rng (Sups ) by Th14;

then inf (rng (Sups )) <= Sup by YELLOW_2:22;

then A10: Inf <= Sup by YELLOW_2:def 6;

( not rng ((curry F) . j) is empty & rng ((curry F) . j) is directed & rng (G . j) is finite Subset of (rng ((curry F) . j)) ) by A2, A5, A7, Lm12;

then consider y being Element of L such that

A11: y in rng ((curry F) . j) and

A12: rng (G . j) is_<=_than y by WAYBEL_0:1;

consider k being object such that

A13: k in dom ((curry F) . j) and

A14: y = ((curry F) . j) . k by A11, FUNCT_1:def 3;

reconsider k = k as Element of K by A13;

take k ; :: thesis: ( k in K & S_{2}[x,k] )

sup (rng (G . j)) <= y by A12, YELLOW_0:32;

then Sup <= y by YELLOW_2:def 5;

hence ( k in K & S_{2}[x,k] )
by A8, A14, A10, ORDERS_2:3; :: thesis: verum

end;( y in K & S

assume x in J ; :: thesis: ex y being object st

( y in K & S

then reconsider j = x as Element of J ;

Sup in rng (Sups ) by Th14;

then inf (rng (Sups )) <= Sup by YELLOW_2:22;

then A10: Inf <= Sup by YELLOW_2:def 6;

( not rng ((curry F) . j) is empty & rng ((curry F) . j) is directed & rng (G . j) is finite Subset of (rng ((curry F) . j)) ) by A2, A5, A7, Lm12;

then consider y being Element of L such that

A11: y in rng ((curry F) . j) and

A12: rng (G . j) is_<=_than y by WAYBEL_0:1;

consider k being object such that

A13: k in dom ((curry F) . j) and

A14: y = ((curry F) . j) . k by A11, FUNCT_1:def 3;

reconsider k = k as Element of K by A13;

take k ; :: thesis: ( k in K & S

sup (rng (G . j)) <= y by A12, YELLOW_0:32;

then Sup <= y by YELLOW_2:def 5;

hence ( k in K & S

A15: dom g = J and

rng g c= K and

A16: for x being object st x in J holds

S

A17: dom (doms (curry F)) = dom (curry F) by FUNCT_6:59;

then A18: dom g = dom (doms (curry F)) by A15, Th20;

for x being object st x in dom (doms (curry F)) holds

g . x in (doms (curry F)) . x

proof

then reconsider g = g as Element of product (doms (curry F)) by A18, CARD_3:9;
let x be object ; :: thesis: ( x in dom (doms (curry F)) implies g . x in (doms (curry F)) . x )

assume x in dom (doms (curry F)) ; :: thesis: g . x in (doms (curry F)) . x

then reconsider j = x as Element of J by A17;

dom (curry F) = J by Th20;

then (doms (curry F)) . j = dom ((curry F) . j) by FUNCT_6:22

.= K by Th20 ;

hence g . x in (doms (curry F)) . x by A16; :: thesis: verum

end;assume x in dom (doms (curry F)) ; :: thesis: g . x in (doms (curry F)) . x

then reconsider j = x as Element of J by A17;

dom (curry F) = J by Th20;

then (doms (curry F)) . j = dom ((curry F) . j) by FUNCT_6:22

.= K by Th20 ;

hence g . x in (doms (curry F)) . x by A16; :: thesis: verum

for j being Element of J holds a <= ((Frege (curry F)) . g) . j

proof

then A20:
a <= Inf
by YELLOW_2:55;
let j be Element of J; :: thesis: a <= ((Frege (curry F)) . g) . j

A19: ex b being Element of L st

( b = ((curry F) . j) . (g . j) & a <= b ) by A16;

( dom (Frege (curry F)) = product (doms (curry F)) & J = dom (curry F) ) by PARTFUN1:def 2;

hence a <= ((Frege (curry F)) . g) . j by A19, Th9; :: thesis: verum

end;A19: ex b being Element of L st

( b = ((curry F) . j) . (g . j) & a <= b ) by A16;

( dom (Frege (curry F)) = product (doms (curry F)) & J = dom (curry F) ) by PARTFUN1:def 2;

hence a <= ((Frege (curry F)) . g) . j by A19, Th9; :: thesis: verum

Inf in rng (Infs ) by Th14;

then Inf <= sup (rng (Infs )) by YELLOW_2:22;

then Inf <= Sup by YELLOW_2:def 5;

hence a9 <= Sup by A3, A20, ORDERS_2:3; :: thesis: verum

then A21: Inf <= Sup by A1;

Inf >= Sup by Th16;

hence Inf = Sup by A21, ORDERS_2:2; :: thesis: verum