let L be complete LATTICE; :: thesis: ( ( 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 ) implies L is continuous )

assume A1: 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 ; :: thesis: L is continuous

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

Inf = Sup

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 ) implies L is continuous )

assume A1: 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 ; :: thesis: L is continuous

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

Inf = Sup

proof

hence
L is continuous
by Lm9; :: thesis: verum
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

Inf = Sup

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

Inf = Sup

let F be DoubleIndexedSet of K,L; :: thesis: ( ( for j being Element of J holds rng (F . j) is directed ) implies Inf = Sup )

set j = the Element of J;

set k = the Element of K . the Element of J;

defpred S_{1}[ set , set , set ] means ( $1 in J & ( ( $2 in K . $1 & $3 = (F . $1) . $2 ) or ( not $2 in K . $1 & $3 = Bottom L ) ) );

A2: dom (doms F) = dom F by FUNCT_6:59;

the Element of J in J ;

then the Element of J in dom K by PARTFUN1:def 2;

then ( the Element of K . the Element of J in K . the Element of J & K . the Element of J in rng K ) by FUNCT_1:def 3;

then reconsider K9 = union (rng K) as non empty set by TARSKI:def 4;

A3: dom F = J by PARTFUN1:def 2;

A4: for j being Element of J

for k9 being Element of K9 ex z being Element of L st S_{1}[j,k9,z]

for j being Element of J

for k being Element of K9 holds S_{1}[j,k,G . (j,k)]
from BINOP_1:sch 3(A4);

then consider G being Function of [:J,K9:], the carrier of L such that

A6: for j being Element of J

for k being Element of K9 holds S_{1}[j,k,G . (j,k)]
;

A7: for j being Element of J holds K . j c= K9

\\/ ((F . j),L) = \\/ (((curry G) . j),L)

A20: dom (curry G) = J by Th20;

product (doms F) c= product (doms (curry G))

then A29: dom (Frege F) c= dom (Frege (curry G)) by PARTFUN1:def 2;

A30: for f being object st f in dom (Frege F) holds

//\ (((Frege F) . f),L) = //\ (((Frege (curry G)) . f),L)

A62: for j being Element of J holds rng ((curry G) . j) is directed

.= dom (curry G) by PARTFUN1:def 2 ;

hence Inf = Inf by A15, Th11

.= Sup by A1, A62, A35 ;

:: thesis: verum

end;for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds

Inf = Sup

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

Inf = Sup

let F be DoubleIndexedSet of K,L; :: thesis: ( ( for j being Element of J holds rng (F . j) is directed ) implies Inf = Sup )

set j = the Element of J;

set k = the Element of K . the Element of J;

defpred S

A2: dom (doms F) = dom F by FUNCT_6:59;

the Element of J in J ;

then the Element of J in dom K by PARTFUN1:def 2;

then ( the Element of K . the Element of J in K . the Element of J & K . the Element of J in rng K ) by FUNCT_1:def 3;

then reconsider K9 = union (rng K) as non empty set by TARSKI:def 4;

A3: dom F = J by PARTFUN1:def 2;

A4: for j being Element of J

for k9 being Element of K9 ex z being Element of L st S

proof

ex G being Function of [:J,K9:], the carrier of L st
let j be Element of J; :: thesis: for k9 being Element of K9 ex z being Element of L st S_{1}[j,k9,z]

let k9 be Element of K9; :: thesis: ex z being Element of L st S_{1}[j,k9,z]

end;let k9 be Element of K9; :: thesis: ex z being Element of L st S

per cases
( k9 in K . j or not k9 in K . j )
;

end;

suppose
k9 in K . j
; :: thesis: ex z being Element of L st S_{1}[j,k9,z]

then reconsider k = k9 as Element of K . j ;

take (F . j) . k ; :: thesis: S_{1}[j,k9,(F . j) . k]

thus S_{1}[j,k9,(F . j) . k]
; :: thesis: verum

end;take (F . j) . k ; :: thesis: S

thus S

for j being Element of J

for k being Element of K9 holds S

then consider G being Function of [:J,K9:], the carrier of L such that

A6: for j being Element of J

for k being Element of K9 holds S

A7: for j being Element of J holds K . j c= K9

proof

A9:
for j being Element of J holds rng (F . j) c= rng ((curry G) . j)
let j be Element of J; :: thesis: K . j c= K9

end;hereby :: according to TARSKI:def 3 :: thesis: verum

let k be object ; :: thesis: ( k in K . j implies k in K9 )

j in J ;

then j in dom K by PARTFUN1:def 2;

then A8: K . j in rng K by FUNCT_1:def 3;

assume k in K . j ; :: thesis: k in K9

hence k in K9 by A8, TARSKI:def 4; :: thesis: verum

end;j in J ;

then j in dom K by PARTFUN1:def 2;

then A8: K . j in rng K by FUNCT_1:def 3;

assume k in K . j ; :: thesis: k in K9

hence k in K9 by A8, TARSKI:def 4; :: thesis: verum

proof

A15:
for j being object st j in dom F holds
let j be Element of J; :: thesis: rng (F . j) c= rng ((curry G) . j)

end;hereby :: according to TARSKI:def 3 :: thesis: verum

let y be object ; :: thesis: ( y in rng (F . j) implies y in rng ((curry G) . j) )

assume y in rng (F . j) ; :: thesis: y in rng ((curry G) . j)

then consider k being object such that

A10: k in dom (F . j) and

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

A12: k in K . j by A10;

K . j c= K9 by A7;

then reconsider k = k as Element of K9 by A12;

[j,k] in [:J,K9:] ;

then A13: [j,k] in dom G by FUNCT_2:def 1;

( k in K9 & dom ((curry G) . j) = (J --> K9) . j ) by FUNCT_2:def 1;

then A14: k in dom ((curry G) . j) ;

y = G . (j,k) by A6, A10, A11

.= ((curry G) . j) . k by A13, FUNCT_5:20 ;

hence y in rng ((curry G) . j) by A14, FUNCT_1:def 3; :: thesis: verum

end;assume y in rng (F . j) ; :: thesis: y in rng ((curry G) . j)

then consider k being object such that

A10: k in dom (F . j) and

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

A12: k in K . j by A10;

K . j c= K9 by A7;

then reconsider k = k as Element of K9 by A12;

[j,k] in [:J,K9:] ;

then A13: [j,k] in dom G by FUNCT_2:def 1;

( k in K9 & dom ((curry G) . j) = (J --> K9) . j ) by FUNCT_2:def 1;

then A14: k in dom ((curry G) . j) ;

y = G . (j,k) by A6, A10, A11

.= ((curry G) . j) . k by A13, FUNCT_5:20 ;

hence y in rng ((curry G) . j) by A14, FUNCT_1:def 3; :: thesis: verum

\\/ ((F . j),L) = \\/ (((curry G) . j),L)

proof

A19:
dom (doms (curry G)) = dom (curry G)
by FUNCT_6:59;
let j9 be object ; :: thesis: ( j9 in dom F implies \\/ ((F . j9),L) = \\/ (((curry G) . j9),L) )

assume j9 in dom F ; :: thesis: \\/ ((F . j9),L) = \\/ (((curry G) . j9),L)

then reconsider j = j9 as Element of J ;

reconsider H = (curry G) . j as Function of ((J --> K9) . j), the carrier of L ;

reconsider H = H as Function of K9, the carrier of L ;

for k being Element of K9 holds H . k <= Sup

( ex_sup_of rng (F . j),L & ex_sup_of rng ((curry G) . j),L ) by YELLOW_0:17;

then sup (rng (F . j)) <= sup (rng ((curry G) . j)) by A9, YELLOW_0:34;

then Sup <= sup (rng H) by YELLOW_2:def 5;

then Sup <= Sup by YELLOW_2:def 5;

hence \\/ ((F . j9),L) = \\/ (((curry G) . j9),L) by A18, ORDERS_2:2; :: thesis: verum

end;assume j9 in dom F ; :: thesis: \\/ ((F . j9),L) = \\/ (((curry G) . j9),L)

then reconsider j = j9 as Element of J ;

reconsider H = (curry G) . j as Function of ((J --> K9) . j), the carrier of L ;

reconsider H = H as Function of K9, the carrier of L ;

for k being Element of K9 holds H . k <= Sup

proof

then A18:
Sup <= Sup
by YELLOW_2:54;
let k be Element of K9; :: thesis: H . k <= Sup

end;per cases
( k in K . j or not k in K . j )
;

end;

suppose A16:
k in K . j
; :: thesis: H . k <= Sup

then A17:
k in dom (F . j)
by FUNCT_2:def 1;

(F . j) . k = G . (j,k) by A6, A16

.= H . k by Th20 ;

then H . k in rng (F . j) by A17, FUNCT_1:def 3;

then H . k <= sup (rng (F . j)) by YELLOW_2:22;

hence H . k <= Sup by YELLOW_2:def 5; :: thesis: verum

end;(F . j) . k = G . (j,k) by A6, A16

.= H . k by Th20 ;

then H . k in rng (F . j) by A17, FUNCT_1:def 3;

then H . k <= sup (rng (F . j)) by YELLOW_2:22;

hence H . k <= Sup by YELLOW_2:def 5; :: thesis: verum

( ex_sup_of rng (F . j),L & ex_sup_of rng ((curry G) . j),L ) by YELLOW_0:17;

then sup (rng (F . j)) <= sup (rng ((curry G) . j)) by A9, YELLOW_0:34;

then Sup <= sup (rng H) by YELLOW_2:def 5;

then Sup <= Sup by YELLOW_2:def 5;

hence \\/ ((F . j9),L) = \\/ (((curry G) . j9),L) by A18, ORDERS_2:2; :: thesis: verum

A20: dom (curry G) = J by Th20;

product (doms F) c= product (doms (curry G))

proof

then
dom (Frege F) c= product (doms (curry G))
;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in product (doms F) or x in product (doms (curry G)) )

assume x in product (doms F) ; :: thesis: x in product (doms (curry G))

then consider g being Function such that

A21: x = g and

A22: dom g = dom (doms F) and

A23: for j being object st j in dom (doms F) holds

g . j in (doms F) . j by CARD_3:def 5;

A24: for j being object st j in dom (doms (curry G)) holds

g . j in (doms (curry G)) . j

hence x in product (doms (curry G)) by A21, A24, CARD_3:def 5; :: thesis: verum

end;assume x in product (doms F) ; :: thesis: x in product (doms (curry G))

then consider g being Function such that

A21: x = g and

A22: dom g = dom (doms F) and

A23: for j being object st j in dom (doms F) holds

g . j in (doms F) . j by CARD_3:def 5;

A24: for j being object st j in dom (doms (curry G)) holds

g . j in (doms (curry G)) . j

proof

dom g = dom (doms (curry G))
by A2, A3, A19, A22, Th20;
let j be object ; :: thesis: ( j in dom (doms (curry G)) implies g . j in (doms (curry G)) . j )

assume A25: j in dom (doms (curry G)) ; :: thesis: g . j in (doms (curry G)) . j

then reconsider j9 = j as Element of J by A19;

j in J by A19, A25;

then A26: g . j in (doms F) . j by A2, A3, A23;

A27: (doms F) . j = dom (F . j9) by A3, FUNCT_6:22

.= K . j9 by FUNCT_2:def 1 ;

A28: K . j9 c= K9 by A7;

(doms (curry G)) . j = dom ((curry G) . j9) by A20, FUNCT_6:22

.= K9 by Th20 ;

hence g . j in (doms (curry G)) . j by A26, A27, A28; :: thesis: verum

end;assume A25: j in dom (doms (curry G)) ; :: thesis: g . j in (doms (curry G)) . j

then reconsider j9 = j as Element of J by A19;

j in J by A19, A25;

then A26: g . j in (doms F) . j by A2, A3, A23;

A27: (doms F) . j = dom (F . j9) by A3, FUNCT_6:22

.= K . j9 by FUNCT_2:def 1 ;

A28: K . j9 c= K9 by A7;

(doms (curry G)) . j = dom ((curry G) . j9) by A20, FUNCT_6:22

.= K9 by Th20 ;

hence g . j in (doms (curry G)) . j by A26, A27, A28; :: thesis: verum

hence x in product (doms (curry G)) by A21, A24, CARD_3:def 5; :: thesis: verum

then A29: dom (Frege F) c= dom (Frege (curry G)) by PARTFUN1:def 2;

A30: for f being object st f in dom (Frege F) holds

//\ (((Frege F) . f),L) = //\ (((Frege (curry G)) . f),L)

proof

A35:
Sup = Sup
let f9 be object ; :: thesis: ( f9 in dom (Frege F) implies //\ (((Frege F) . f9),L) = //\ (((Frege (curry G)) . f9),L) )

assume A31: f9 in dom (Frege F) ; :: thesis: //\ (((Frege F) . f9),L) = //\ (((Frege (curry G)) . f9),L)

then reconsider f = f9 as Element of product (doms F) ;

A32: dom ((Frege F) . f) = dom F by A31, Th8

.= J by PARTFUN1:def 2 ;

A33: for j being object st j in J holds

((Frege F) . f) . j = ((Frege (curry G)) . f) . j

.= proj1 (dom G) by FUNCT_5:def 1

.= proj1 [:J,K9:] by FUNCT_2:def 1

.= J by FUNCT_5:9 ;

hence //\ (((Frege F) . f9),L) = //\ (((Frege (curry G)) . f9),L) by A32, A33, FUNCT_1:2; :: thesis: verum

end;assume A31: f9 in dom (Frege F) ; :: thesis: //\ (((Frege F) . f9),L) = //\ (((Frege (curry G)) . f9),L)

then reconsider f = f9 as Element of product (doms F) ;

A32: dom ((Frege F) . f) = dom F by A31, Th8

.= J by PARTFUN1:def 2 ;

A33: for j being object st j in J holds

((Frege F) . f) . j = ((Frege (curry G)) . f) . j

proof

dom ((Frege (curry G)) . f) =
dom (curry G)
by A29, A31, Th8
let j9 be object ; :: thesis: ( j9 in J implies ((Frege F) . f) . j9 = ((Frege (curry G)) . f) . j9 )

assume j9 in J ; :: thesis: ((Frege F) . f) . j9 = ((Frege (curry G)) . f) . j9

then reconsider j = j9 as Element of J ;

A34: f . j in K . j by A31, Lm6;

K . j c= K9 by A7;

then reconsider fj = f . j as Element of K9 by A34;

((Frege F) . f) . j = (F . j) . fj by A31, Lm5

.= G . (j,fj) by A6, A34

.= ((curry G) . j) . (f . j) by Th20

.= ((Frege (curry G)) . f) . j by A29, A31, Lm5 ;

hence ((Frege F) . f) . j9 = ((Frege (curry G)) . f) . j9 ; :: thesis: verum

end;assume j9 in J ; :: thesis: ((Frege F) . f) . j9 = ((Frege (curry G)) . f) . j9

then reconsider j = j9 as Element of J ;

A34: f . j in K . j by A31, Lm6;

K . j c= K9 by A7;

then reconsider fj = f . j as Element of K9 by A34;

((Frege F) . f) . j = (F . j) . fj by A31, Lm5

.= G . (j,fj) by A6, A34

.= ((curry G) . j) . (f . j) by Th20

.= ((Frege (curry G)) . f) . j by A29, A31, Lm5 ;

hence ((Frege F) . f) . j9 = ((Frege (curry G)) . f) . j9 ; :: thesis: verum

.= proj1 (dom G) by FUNCT_5:def 1

.= proj1 [:J,K9:] by FUNCT_2:def 1

.= J by FUNCT_5:9 ;

hence //\ (((Frege F) . f9),L) = //\ (((Frege (curry G)) . f9),L) by A32, A33, FUNCT_1:2; :: thesis: verum

proof
end;

assume A61:
for j being Element of J holds rng (F . j) is directed
; :: thesis: Inf = Sup per cases
( for j being Element of J holds K . j = K9 or ex j being Element of J st K . j <> K9 )
;

end;

suppose A36:
for j being Element of J holds K . j = K9
; :: thesis: Sup = Sup

for j being object st j in J holds

(doms F) . j = (doms (curry G)) . j

then dom (Frege F) = product (doms (curry G)) by PARTFUN1:def 2;

then dom (Frege F) = dom (Frege (curry G)) by PARTFUN1:def 2;

hence Sup = Sup by A30, Th12; :: thesis: verum

end;(doms F) . j = (doms (curry G)) . j

proof

then
doms F = doms (curry G)
by A2, A3, A19, A20, FUNCT_1:2;
let j be object ; :: thesis: ( j in J implies (doms F) . j = (doms (curry G)) . j )

assume j in J ; :: thesis: (doms F) . j = (doms (curry G)) . j

then reconsider j9 = j as Element of J ;

A37: (doms F) . j = dom (F . j9) by A3, FUNCT_6:22

.= K . j9 by FUNCT_2:def 1 ;

(doms (curry G)) . j = dom ((curry G) . j9) by A20, FUNCT_6:22

.= K9 by Th20 ;

hence (doms F) . j = (doms (curry G)) . j by A36, A37; :: thesis: verum

end;assume j in J ; :: thesis: (doms F) . j = (doms (curry G)) . j

then reconsider j9 = j as Element of J ;

A37: (doms F) . j = dom (F . j9) by A3, FUNCT_6:22

.= K . j9 by FUNCT_2:def 1 ;

(doms (curry G)) . j = dom ((curry G) . j9) by A20, FUNCT_6:22

.= K9 by Th20 ;

hence (doms F) . j = (doms (curry G)) . j by A36, A37; :: thesis: verum

then dom (Frege F) = product (doms (curry G)) by PARTFUN1:def 2;

then dom (Frege F) = dom (Frege (curry G)) by PARTFUN1:def 2;

hence Sup = Sup by A30, Th12; :: thesis: verum

suppose
ex j being Element of J st K . j <> K9
; :: thesis: Sup = Sup

then consider j being Element of J such that

A38: K . j <> K9 ;

K . j c= K9 by A7;

then not K9 c= K . j by A38, XBOOLE_0:def 10;

then consider k being object such that

A39: k in K9 and

A40: not k in K . j ;

reconsider k = k as Element of K9 by A39;

A41: (rng (Infs )) \/ {(Bottom L)} c= rng (Infs )

A52: rng (Infs ) c= (rng (Infs )) \/ {(Bottom L)}

Sup = sup (rng (Infs )) by YELLOW_2:def 5

.= sup ((rng (Infs )) \/ {(Bottom L)}) by A52, A41, XBOOLE_0:def 10

.= (sup (rng (Infs ))) "\/" (sup {(Bottom L)}) by A51, YELLOW_2:3

.= (sup (rng (Infs ))) "\/" (Bottom L) by YELLOW_0:39

.= (Sup ) "\/" (Bottom L) by YELLOW_2:def 5

.= Sup by A60, YELLOW_0:24 ;

hence Sup = Sup ; :: thesis: verum

end;A38: K . j <> K9 ;

K . j c= K9 by A7;

then not K9 c= K . j by A38, XBOOLE_0:def 10;

then consider k being object such that

A39: k in K9 and

A40: not k in K . j ;

reconsider k = k as Element of K9 by A39;

A41: (rng (Infs )) \/ {(Bottom L)} c= rng (Infs )

proof

A51:
( ex_sup_of rng (Infs ),L & ex_sup_of {(Bottom L)},L )
by YELLOW_0:17;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (rng (Infs )) \/ {(Bottom L)} or x in rng (Infs ) )

assume A42: x in (rng (Infs )) \/ {(Bottom L)} ; :: thesis: x in rng (Infs )

end;assume A42: x in (rng (Infs )) \/ {(Bottom L)} ; :: thesis: x in rng (Infs )

per cases
( x in rng (Infs ) or x in {(Bottom L)} )
by A42, XBOOLE_0:def 3;

end;

suppose
x in rng (Infs )
; :: thesis: x in rng (Infs )

then consider f being object such that

A43: f in dom (Frege F) and

A44: x = //\ (((Frege F) . f),L) by Th13;

x = //\ (((Frege (curry G)) . f),L) by A30, A43, A44;

hence x in rng (Infs ) by A29, A43, Th13; :: thesis: verum

end;A43: f in dom (Frege F) and

A44: x = //\ (((Frege F) . f),L) by Th13;

x = //\ (((Frege (curry G)) . f),L) by A30, A43, A44;

hence x in rng (Infs ) by A29, A43, Th13; :: thesis: verum

suppose A45:
x in {(Bottom L)}
; :: thesis: x in rng (Infs )

then reconsider x9 = x as Element of L ;

set f = J --> k;

A46: for x being object st x in dom (doms (curry G)) holds

(J --> k) . x in (doms (curry G)) . x

.= dom (doms (curry G)) by A19, Th20 ;

then J --> k in product (doms (curry G)) by A46, CARD_3:9;

then A48: J --> k in dom (Frege (curry G)) by PARTFUN1:def 2;

A49: x = Bottom L by A45, TARSKI:def 1;

then x = G . (j,k) by A6, A40

.= ((curry G) . j) . k by Th20

.= ((curry G) . j) . ((J --> k) . j) ;

then x in rng ((Frege (curry G)) . (J --> k)) by A48, Lm5;

then x9 >= "/\" ((rng ((Frege (curry G)) . (J --> k))),L) by YELLOW_2:22;

then A50: x9 >= //\ (((Frege (curry G)) . (J --> k)),L) by YELLOW_2:def 6;

x9 <= //\ (((Frege (curry G)) . (J --> k)),L) by A49, YELLOW_0:44;

then x9 = //\ (((Frege (curry G)) . (J --> k)),L) by A50, ORDERS_2:2;

hence x in rng (Infs ) by A48, Th13; :: thesis: verum

end;set f = J --> k;

A46: for x being object st x in dom (doms (curry G)) holds

(J --> k) . x in (doms (curry G)) . x

proof

dom (J --> k) =
J
let x be object ; :: thesis: ( x in dom (doms (curry G)) implies (J --> k) . x in (doms (curry G)) . x )

assume x in dom (doms (curry G)) ; :: thesis: (J --> k) . x in (doms (curry G)) . x

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

(doms (curry G)) . j = dom ((curry G) . j) by A20, FUNCT_6:22

.= K9 by Th20 ;

hence (J --> k) . x in (doms (curry G)) . x ; :: thesis: verum

end;assume x in dom (doms (curry G)) ; :: thesis: (J --> k) . x in (doms (curry G)) . x

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

(doms (curry G)) . j = dom ((curry G) . j) by A20, FUNCT_6:22

.= K9 by Th20 ;

hence (J --> k) . x in (doms (curry G)) . x ; :: thesis: verum

.= dom (doms (curry G)) by A19, Th20 ;

then J --> k in product (doms (curry G)) by A46, CARD_3:9;

then A48: J --> k in dom (Frege (curry G)) by PARTFUN1:def 2;

A49: x = Bottom L by A45, TARSKI:def 1;

then x = G . (j,k) by A6, A40

.= ((curry G) . j) . k by Th20

.= ((curry G) . j) . ((J --> k) . j) ;

then x in rng ((Frege (curry G)) . (J --> k)) by A48, Lm5;

then x9 >= "/\" ((rng ((Frege (curry G)) . (J --> k))),L) by YELLOW_2:22;

then A50: x9 >= //\ (((Frege (curry G)) . (J --> k)),L) by YELLOW_2:def 6;

x9 <= //\ (((Frege (curry G)) . (J --> k)),L) by A49, YELLOW_0:44;

then x9 = //\ (((Frege (curry G)) . (J --> k)),L) by A50, ORDERS_2:2;

hence x in rng (Infs ) by A48, Th13; :: thesis: verum

A52: rng (Infs ) c= (rng (Infs )) \/ {(Bottom L)}

proof

A60:
Bottom L <= Sup
by YELLOW_0:44;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (Infs ) or x in (rng (Infs )) \/ {(Bottom L)} )

assume x in rng (Infs ) ; :: thesis: x in (rng (Infs )) \/ {(Bottom L)}

then consider f being object such that

A53: f in dom (Frege (curry G)) and

A54: x = //\ (((Frege (curry G)) . f),L) by Th13;

reconsider f = f as Function by A53;

end;assume x in rng (Infs ) ; :: thesis: x in (rng (Infs )) \/ {(Bottom L)}

then consider f being object such that

A53: f in dom (Frege (curry G)) and

A54: x = //\ (((Frege (curry G)) . f),L) by Th13;

reconsider f = f as Function by A53;

per cases
( for j being Element of J holds f . j in K . j or ex j being Element of J st not f . j in K . j )
;

end;

suppose A55:
for j being Element of J holds f . j in K . j
; :: thesis: x in (rng (Infs )) \/ {(Bottom L)}

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

f . x in (doms F) . x

.= dom (doms F) by A2, A3, Th20 ;

then f in product (doms F) by A56, CARD_3:9;

then A57: f in dom (Frege F) by PARTFUN1:def 2;

then x = //\ (((Frege F) . f),L) by A30, A54;

then x in rng (Infs ) by A57, Th13;

hence x in (rng (Infs )) \/ {(Bottom L)} by XBOOLE_0:def 3; :: thesis: verum

end;f . x in (doms F) . x

proof

dom f =
dom (curry G)
by A53, Th8
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 reconsider j = x as Element of J by A3, FUNCT_6:59;

(doms F) . j = dom (F . j) by A3, FUNCT_6:22

.= K . j by FUNCT_2:def 1 ;

hence f . x in (doms F) . x by A55; :: thesis: verum

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

then reconsider j = x as Element of J by A3, FUNCT_6:59;

(doms F) . j = dom (F . j) by A3, FUNCT_6:22

.= K . j by FUNCT_2:def 1 ;

hence f . x in (doms F) . x by A55; :: thesis: verum

.= dom (doms F) by A2, A3, Th20 ;

then f in product (doms F) by A56, CARD_3:9;

then A57: f in dom (Frege F) by PARTFUN1:def 2;

then x = //\ (((Frege F) . f),L) by A30, A54;

then x in rng (Infs ) by A57, Th13;

hence x in (rng (Infs )) \/ {(Bottom L)} by XBOOLE_0:def 3; :: thesis: verum

suppose
not for j being Element of J holds f . j in K . j
; :: thesis: x in (rng (Infs )) \/ {(Bottom L)}

then consider j being Element of J such that

A58: not f . j in K . j ;

j in J ;

then j in dom (curry G) by Th20;

then f . j in dom ((curry G) . j) by A53, Th9;

then reconsider k = f . j as Element of K9 ;

Bottom L = G . (j,k) by A6, A58

.= ((curry G) . j) . (f . j) by Th20 ;

then Bottom L in rng ((Frege (curry G)) . f) by A53, Lm5;

then Bottom L >= "/\" ((rng ((Frege (curry G)) . f)),L) by YELLOW_2:22;

then A59: Bottom L >= //\ (((Frege (curry G)) . f),L) by YELLOW_2:def 6;

Bottom L <= //\ (((Frege (curry G)) . f),L) by YELLOW_0:44;

then x = Bottom L by A54, A59, ORDERS_2:2;

then x in {(Bottom L)} by TARSKI:def 1;

hence x in (rng (Infs )) \/ {(Bottom L)} by XBOOLE_0:def 3; :: thesis: verum

end;A58: not f . j in K . j ;

j in J ;

then j in dom (curry G) by Th20;

then f . j in dom ((curry G) . j) by A53, Th9;

then reconsider k = f . j as Element of K9 ;

Bottom L = G . (j,k) by A6, A58

.= ((curry G) . j) . (f . j) by Th20 ;

then Bottom L in rng ((Frege (curry G)) . f) by A53, Lm5;

then Bottom L >= "/\" ((rng ((Frege (curry G)) . f)),L) by YELLOW_2:22;

then A59: Bottom L >= //\ (((Frege (curry G)) . f),L) by YELLOW_2:def 6;

Bottom L <= //\ (((Frege (curry G)) . f),L) by YELLOW_0:44;

then x = Bottom L by A54, A59, ORDERS_2:2;

then x in {(Bottom L)} by TARSKI:def 1;

hence x in (rng (Infs )) \/ {(Bottom L)} by XBOOLE_0:def 3; :: thesis: verum

Sup = sup (rng (Infs )) by YELLOW_2:def 5

.= sup ((rng (Infs )) \/ {(Bottom L)}) by A52, A41, XBOOLE_0:def 10

.= (sup (rng (Infs ))) "\/" (sup {(Bottom L)}) by A51, YELLOW_2:3

.= (sup (rng (Infs ))) "\/" (Bottom L) by YELLOW_0:39

.= (Sup ) "\/" (Bottom L) by YELLOW_2:def 5

.= Sup by A60, YELLOW_0:24 ;

hence Sup = Sup ; :: thesis: verum

A62: for j being Element of J holds rng ((curry G) . j) is directed

proof

dom F =
J
by PARTFUN1:def 2
let j be Element of J; :: thesis: rng ((curry G) . j) is directed

set X = rng ((curry G) . j);

for x, y being Element of L st x in rng ((curry G) . j) & y in rng ((curry G) . j) holds

ex z being Element of L st

( z in rng ((curry G) . j) & x <= z & y <= z )

end;set X = rng ((curry G) . j);

for x, y being Element of L st x in rng ((curry G) . j) & y in rng ((curry G) . j) holds

ex z being Element of L st

( z in rng ((curry G) . j) & x <= z & y <= z )

proof

hence
rng ((curry G) . j) is directed
by WAYBEL_0:def 1; :: thesis: verum
A63:
rng (F . j) is directed
by A61;

let x, y be Element of L; :: thesis: ( x in rng ((curry G) . j) & y in rng ((curry G) . j) implies ex z being Element of L st

( z in rng ((curry G) . j) & x <= z & y <= z ) )

assume that

A64: x in rng ((curry G) . j) and

A65: y in rng ((curry G) . j) ; :: thesis: ex z being Element of L st

( z in rng ((curry G) . j) & x <= z & y <= z )

consider b being object such that

A66: b in dom ((curry G) . j) and

A67: ((curry G) . j) . b = y by A65, FUNCT_1:def 3;

consider a being object such that

A68: a in dom ((curry G) . j) and

A69: ((curry G) . j) . a = x by A64, FUNCT_1:def 3;

reconsider a9 = a, b9 = b as Element of K9 by A68, A66;

A70: x = G . (j,a9) by A69, Th20;

A71: y = G . (j,b9) by A67, Th20;

end;let x, y be Element of L; :: thesis: ( x in rng ((curry G) . j) & y in rng ((curry G) . j) implies ex z being Element of L st

( z in rng ((curry G) . j) & x <= z & y <= z ) )

assume that

A64: x in rng ((curry G) . j) and

A65: y in rng ((curry G) . j) ; :: thesis: ex z being Element of L st

( z in rng ((curry G) . j) & x <= z & y <= z )

consider b being object such that

A66: b in dom ((curry G) . j) and

A67: ((curry G) . j) . b = y by A65, FUNCT_1:def 3;

consider a being object such that

A68: a in dom ((curry G) . j) and

A69: ((curry G) . j) . a = x by A64, FUNCT_1:def 3;

reconsider a9 = a, b9 = b as Element of K9 by A68, A66;

A70: x = G . (j,a9) by A69, Th20;

A71: y = G . (j,b9) by A67, Th20;

per cases
( ( a in K . j & b in K . j ) or ( a in K . j & not b in K . j ) or ( not a in K . j & b in K . j ) or ( not a in K . j & not b in K . j ) )
;

end;

suppose A72:
( a in K . j & b in K . j )
; :: thesis: ex z being Element of L st

( z in rng ((curry G) . j) & x <= z & y <= z )

( z in rng ((curry G) . j) & x <= z & y <= z )

then
( b in dom (F . j) & y = (F . j) . b9 )
by A6, A71, FUNCT_2:def 1;

then A73: y in rng (F . j) by FUNCT_1:def 3;

( a in dom (F . j) & x = (F . j) . a9 ) by A6, A70, A72, FUNCT_2:def 1;

then x in rng (F . j) by FUNCT_1:def 3;

then consider z being Element of L such that

A74: ( z in rng (F . j) & x <= z & y <= z ) by A63, A73, WAYBEL_0:def 1;

take z ; :: thesis: ( z in rng ((curry G) . j) & x <= z & y <= z )

rng (F . j) c= rng ((curry G) . j) by A9;

hence ( z in rng ((curry G) . j) & x <= z & y <= z ) by A74; :: thesis: verum

end;then A73: y in rng (F . j) by FUNCT_1:def 3;

( a in dom (F . j) & x = (F . j) . a9 ) by A6, A70, A72, FUNCT_2:def 1;

then x in rng (F . j) by FUNCT_1:def 3;

then consider z being Element of L such that

A74: ( z in rng (F . j) & x <= z & y <= z ) by A63, A73, WAYBEL_0:def 1;

take z ; :: thesis: ( z in rng ((curry G) . j) & x <= z & y <= z )

rng (F . j) c= rng ((curry G) . j) by A9;

hence ( z in rng ((curry G) . j) & x <= z & y <= z ) by A74; :: thesis: verum

suppose A75:
( a in K . j & not b in K . j )
; :: thesis: ex z being Element of L st

( z in rng ((curry G) . j) & x <= z & y <= z )

( z in rng ((curry G) . j) & x <= z & y <= z )

take
x
; :: thesis: ( x in rng ((curry G) . j) & x <= x & y <= x )

y = Bottom L by A6, A71, A75;

hence ( x in rng ((curry G) . j) & x <= x & y <= x ) by A64, YELLOW_0:44; :: thesis: verum

end;y = Bottom L by A6, A71, A75;

hence ( x in rng ((curry G) . j) & x <= x & y <= x ) by A64, YELLOW_0:44; :: thesis: verum

suppose A76:
( not a in K . j & b in K . j )
; :: thesis: ex z being Element of L st

( z in rng ((curry G) . j) & x <= z & y <= z )

( z in rng ((curry G) . j) & x <= z & y <= z )

take
y
; :: thesis: ( y in rng ((curry G) . j) & x <= y & y <= y )

x = Bottom L by A6, A70, A76;

hence ( y in rng ((curry G) . j) & x <= y & y <= y ) by A65, YELLOW_0:44; :: thesis: verum

end;x = Bottom L by A6, A70, A76;

hence ( y in rng ((curry G) . j) & x <= y & y <= y ) by A65, YELLOW_0:44; :: thesis: verum

suppose A77:
( not a in K . j & not b in K . j )
; :: thesis: ex z being Element of L st

( z in rng ((curry G) . j) & x <= z & y <= z )

( z in rng ((curry G) . j) & x <= z & y <= z )

take
x
; :: thesis: ( x in rng ((curry G) . j) & x <= x & y <= x )

x = Bottom L by A6, A70, A77;

hence ( x in rng ((curry G) . j) & x <= x & y <= x ) by A6, A64, A71, A77; :: thesis: verum

end;x = Bottom L by A6, A70, A77;

hence ( x in rng ((curry G) . j) & x <= x & y <= x ) by A6, A64, A71, A77; :: thesis: verum

.= dom (curry G) by PARTFUN1:def 2 ;

hence Inf = Inf by A15, Th11

.= Sup by A1, A62, A35 ;

:: thesis: verum