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

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

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 )

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

hereby :: thesis: verum

let J, K be non empty set ; :: thesis: 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

set FIK = { A where A is Subset of K : ( A is finite & A <> {} ) } ;

set k = the Element of K;

{ the Element of K} in { A where A is Subset of K : ( A is finite & A <> {} ) } ;

then reconsider FIK = { A where A is Subset of K : ( A is finite & A <> {} ) } as non empty set ;

let F be Function of [:J,K:], the carrier of L; :: thesis: 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

let X be Subset of L; :: thesis: ( 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 ) ) } implies Inf = sup X )

set N = Funcs (J,FIK);

deffunc H_{1}( Element of J, Element of Funcs (J,FIK)) -> Element of the carrier of L = sup (((curry F) . $1) .: ($2 . $1));

ex H being Function of [:J,(Funcs (J,FIK)):], the carrier of L st

for j being Element of J

for g being Element of Funcs (J,FIK) holds H . (j,g) = H_{1}(j,g)
from BINOP_1:sch 4();

then consider H being Function of [:J,(Funcs (J,FIK)):], the carrier of L such that

A2: for j being Element of J

for g being Element of Funcs (J,FIK) holds H . (j,g) = sup (((curry F) . j) .: (g . j)) ;

set cF = curry F;

set cH = curry H;

A3: for j being Element of J holds

( ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds

ex_sup_of Y,L ) & ( for x being Element of L st x in rng ((curry H) . j) holds

ex Y being finite Subset of (rng ((curry F) . j)) st

( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds

"\/" (Y,L) in rng ((curry H) . j) ) )

A15: for j being object st j in dom (curry F) holds

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

( 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 ) ) } ; :: thesis: Inf = sup X

then A18: Inf >= sup X by Th22;

A19: FIK c= Fin K

( ( for j being Element of J holds

( ((Frege h) . (id J)) . j = (h . j) . j & h . j in Funcs (J,FIK) & ((Frege h) . (id J)) . j is non empty finite Subset of K ) ) & (Frege h) . (id J) is V9() ManySortedSet of J & (Frege h) . (id J) in Funcs (J,FIK) & (Frege h) . (id J) in Funcs (J,(Fin K)) )

dom (curry F) = J by Th20

.= dom (curry H) by Th20 ;

then Inf = Inf by A15, Th11;

then Inf <= sup X by A14, A53, YELLOW_2:def 5;

hence Inf = sup X by A18, ORDERS_2:2; :: thesis: verum

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

set FIK = { A where A is Subset of K : ( A is finite & A <> {} ) } ;

set k = the Element of K;

{ the Element of K} in { A where A is Subset of K : ( A is finite & A <> {} ) } ;

then reconsider FIK = { A where A is Subset of K : ( A is finite & A <> {} ) } as non empty set ;

let F be Function of [:J,K:], the carrier of L; :: thesis: 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

let X be Subset of L; :: thesis: ( 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 ) ) } implies Inf = sup X )

set N = Funcs (J,FIK);

deffunc H

ex H being Function of [:J,(Funcs (J,FIK)):], the carrier of L st

for j being Element of J

for g being Element of Funcs (J,FIK) holds H . (j,g) = H

then consider H being Function of [:J,(Funcs (J,FIK)):], the carrier of L such that

A2: for j being Element of J

for g being Element of Funcs (J,FIK) holds H . (j,g) = sup (((curry F) . j) .: (g . j)) ;

set cF = curry F;

set cH = curry H;

A3: for j being Element of J holds

( ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds

ex_sup_of Y,L ) & ( for x being Element of L st x in rng ((curry H) . j) holds

ex Y being finite Subset of (rng ((curry F) . j)) st

( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds

"\/" (Y,L) in rng ((curry H) . j) ) )

proof

for j being Element of J holds rng ((curry H) . j) is directed
let j be Element of J; :: thesis: ( ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds

ex_sup_of Y,L ) & ( for x being Element of L st x in rng ((curry H) . j) holds

ex Y being finite Subset of (rng ((curry F) . j)) st

( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds

"\/" (Y,L) in rng ((curry H) . j) ) )

set D = rng ((curry H) . j);

set R = rng ((curry F) . j);

set Hj = (curry H) . j;

set Fj = (curry F) . j;

thus for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds

ex_sup_of Y,L by YELLOW_0:17; :: thesis: ( ( for x being Element of L st x in rng ((curry H) . j) holds

ex Y being finite Subset of (rng ((curry F) . j)) st

( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds

"\/" (Y,L) in rng ((curry H) . j) ) )

thus for x being Element of L st x in rng ((curry H) . j) holds

ex Y being finite Subset of (rng ((curry F) . j)) st

( ex_sup_of Y,L & x = "\/" (Y,L) ) :: thesis: for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds

"\/" (Y,L) in rng ((curry H) . j)

"\/" (Y,L) in rng ((curry H) . j) :: thesis: verum

end;ex_sup_of Y,L ) & ( for x being Element of L st x in rng ((curry H) . j) holds

ex Y being finite Subset of (rng ((curry F) . j)) st

( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds

"\/" (Y,L) in rng ((curry H) . j) ) )

set D = rng ((curry H) . j);

set R = rng ((curry F) . j);

set Hj = (curry H) . j;

set Fj = (curry F) . j;

thus for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds

ex_sup_of Y,L by YELLOW_0:17; :: thesis: ( ( for x being Element of L st x in rng ((curry H) . j) holds

ex Y being finite Subset of (rng ((curry F) . j)) st

( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds

"\/" (Y,L) in rng ((curry H) . j) ) )

thus for x being Element of L st x in rng ((curry H) . j) holds

ex Y being finite Subset of (rng ((curry F) . j)) st

( ex_sup_of Y,L & x = "\/" (Y,L) ) :: thesis: for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds

"\/" (Y,L) in rng ((curry H) . j)

proof

thus
for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds
let x be Element of L; :: thesis: ( x in rng ((curry H) . j) implies ex Y being finite Subset of (rng ((curry F) . j)) st

( ex_sup_of Y,L & x = "\/" (Y,L) ) )

assume x in rng ((curry H) . j) ; :: thesis: ex Y being finite Subset of (rng ((curry F) . j)) st

( ex_sup_of Y,L & x = "\/" (Y,L) )

then consider g being object such that

A4: g in dom ((curry H) . j) and

A5: ((curry H) . j) . g = x by FUNCT_1:def 3;

reconsider g = g as Element of Funcs (J,FIK) by A4;

g . j in FIK ;

then ex A being Subset of K st

( A = g . j & A is finite & A <> {} ) ;

then reconsider Y = ((curry F) . j) .: (g . j) as finite Subset of (rng ((curry F) . j)) by RELAT_1:111;

take Y ; :: thesis: ( ex_sup_of Y,L & x = "\/" (Y,L) )

x = H . (j,g) by A5, Th20

.= sup (((curry F) . j) .: (g . j)) by A2 ;

hence ( ex_sup_of Y,L & x = "\/" (Y,L) ) by YELLOW_0:17; :: thesis: verum

end;( ex_sup_of Y,L & x = "\/" (Y,L) ) )

assume x in rng ((curry H) . j) ; :: thesis: ex Y being finite Subset of (rng ((curry F) . j)) st

( ex_sup_of Y,L & x = "\/" (Y,L) )

then consider g being object such that

A4: g in dom ((curry H) . j) and

A5: ((curry H) . j) . g = x by FUNCT_1:def 3;

reconsider g = g as Element of Funcs (J,FIK) by A4;

g . j in FIK ;

then ex A being Subset of K st

( A = g . j & A is finite & A <> {} ) ;

then reconsider Y = ((curry F) . j) .: (g . j) as finite Subset of (rng ((curry F) . j)) by RELAT_1:111;

take Y ; :: thesis: ( ex_sup_of Y,L & x = "\/" (Y,L) )

x = H . (j,g) by A5, Th20

.= sup (((curry F) . j) .: (g . j)) by A2 ;

hence ( ex_sup_of Y,L & x = "\/" (Y,L) ) by YELLOW_0:17; :: thesis: verum

"\/" (Y,L) in rng ((curry H) . j) :: thesis: verum

proof

let Y be finite Subset of (rng ((curry F) . j)); :: thesis: ( Y <> {} implies "\/" (Y,L) in rng ((curry H) . j) )

consider Z being set such that

A6: Z c= dom ((curry F) . j) and

A7: Z is finite and

A8: ((curry F) . j) .: Z = Y by ORDERS_1:85;

A9: Z c= K by A6, Th20;

assume Y <> {} ; :: thesis: "\/" (Y,L) in rng ((curry H) . j)

then Z <> {} by A8;

then Z in FIK by A7, A9;

then A10: {Z} c= FIK by ZFMISC_1:31;

( dom (J --> Z) = J & rng (J --> Z) = {Z} ) by FUNCOP_1:8;

then reconsider g = J --> Z as Element of Funcs (J,FIK) by A10, FUNCT_2:def 2;

A11: g . j = Z ;

g in Funcs (J,FIK) ;

then A12: g in dom ((curry H) . j) by Th20;

((curry H) . j) . g = H . (j,g) by Th20

.= "\/" (Y,L) by A2, A8, A11 ;

hence "\/" (Y,L) in rng ((curry H) . j) by A12, FUNCT_1:def 3; :: thesis: verum

end;consider Z being set such that

A6: Z c= dom ((curry F) . j) and

A7: Z is finite and

A8: ((curry F) . j) .: Z = Y by ORDERS_1:85;

A9: Z c= K by A6, Th20;

assume Y <> {} ; :: thesis: "\/" (Y,L) in rng ((curry H) . j)

then Z <> {} by A8;

then Z in FIK by A7, A9;

then A10: {Z} c= FIK by ZFMISC_1:31;

( dom (J --> Z) = J & rng (J --> Z) = {Z} ) by FUNCOP_1:8;

then reconsider g = J --> Z as Element of Funcs (J,FIK) by A10, FUNCT_2:def 2;

A11: g . j = Z ;

g in Funcs (J,FIK) ;

then A12: g in dom ((curry H) . j) by Th20;

((curry H) . j) . g = H . (j,g) by Th20

.= "\/" (Y,L) by A2, A8, A11 ;

hence "\/" (Y,L) in rng ((curry H) . j) by A12, FUNCT_1:def 3; :: thesis: verum

proof

then A14:
Inf = Sup
by A1, Lm8;
let j be Element of J; :: thesis: rng ((curry H) . j) is directed

A13: for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds

"\/" (Y,L) in rng ((curry H) . j) by A3;

( ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds

ex_sup_of Y,L ) & ( for x being Element of L st x in rng ((curry H) . j) holds

ex Y being finite Subset of (rng ((curry F) . j)) st

( ex_sup_of Y,L & x = "\/" (Y,L) ) ) ) by A3;

hence rng ((curry H) . j) is directed by A13, WAYBEL_0:51; :: thesis: verum

end;A13: for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds

"\/" (Y,L) in rng ((curry H) . j) by A3;

( ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds

ex_sup_of Y,L ) & ( for x being Element of L st x in rng ((curry H) . j) holds

ex Y being finite Subset of (rng ((curry F) . j)) st

( ex_sup_of Y,L & x = "\/" (Y,L) ) ) ) by A3;

hence rng ((curry H) . j) is directed by A13, WAYBEL_0:51; :: thesis: verum

A15: for j being object st j in dom (curry F) holds

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

proof

assume A17:
X = { a where a is Element of L : ex f being V9() ManySortedSet of J st
let j9 be object ; :: thesis: ( j9 in dom (curry F) implies \\/ (((curry F) . j9),L) = \\/ (((curry H) . j9),L) )

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

then reconsider j = j9 as Element of J ;

A16: ( ( for x being Element of L st x in rng ((curry H) . j) holds

ex Y being finite Subset of (rng ((curry F) . j)) st

( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds

"\/" (Y,L) in rng ((curry H) . j) ) ) by A3;

( ex_sup_of rng ((curry F) . j),L & ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds

ex_sup_of Y,L ) ) by YELLOW_0:17;

then sup (rng ((curry F) . j)) = sup (rng ((curry H) . j)) by A16, WAYBEL_0:54;

then Sup = sup (rng ((curry H) . j)) by YELLOW_2:def 5;

hence \\/ (((curry F) . j9),L) = \\/ (((curry H) . j9),L) by YELLOW_2:def 5; :: thesis: verum

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

then reconsider j = j9 as Element of J ;

A16: ( ( for x being Element of L st x in rng ((curry H) . j) holds

ex Y being finite Subset of (rng ((curry F) . j)) st

( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds

"\/" (Y,L) in rng ((curry H) . j) ) ) by A3;

( ex_sup_of rng ((curry F) . j),L & ( for Y being finite Subset of (rng ((curry F) . j)) st Y <> {} holds

ex_sup_of Y,L ) ) by YELLOW_0:17;

then sup (rng ((curry F) . j)) = sup (rng ((curry H) . j)) by A16, WAYBEL_0:54;

then Sup = sup (rng ((curry H) . j)) by YELLOW_2:def 5;

hence \\/ (((curry F) . j9),L) = \\/ (((curry H) . j9),L) by YELLOW_2:def 5; :: thesis: verum

( 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 ) ) } ; :: thesis: Inf = sup X

then A18: Inf >= sup X by Th22;

A19: FIK c= Fin K

proof

A20:
for h being Function-yielding Function st h in product (doms (curry H)) holds
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in FIK or x in Fin K )

assume x in FIK ; :: thesis: x in Fin K

then ex A being Subset of K st

( x = A & A is finite & A <> {} ) ;

hence x in Fin K by FINSUB_1:def 5; :: thesis: verum

end;assume x in FIK ; :: thesis: x in Fin K

then ex A being Subset of K st

( x = A & A is finite & A <> {} ) ;

hence x in Fin K by FINSUB_1:def 5; :: thesis: verum

( ( for j being Element of J holds

( ((Frege h) . (id J)) . j = (h . j) . j & h . j in Funcs (J,FIK) & ((Frege h) . (id J)) . j is non empty finite Subset of K ) ) & (Frege h) . (id J) is V9() ManySortedSet of J & (Frege h) . (id J) in Funcs (J,FIK) & (Frege h) . (id J) in Funcs (J,(Fin K)) )

proof

A33:
for h being Element of product (doms (curry H)) holds Inf <= sup X
let h be Function-yielding Function; :: thesis: ( h in product (doms (curry H)) implies ( ( for j being Element of J holds

( ((Frege h) . (id J)) . j = (h . j) . j & h . j in Funcs (J,FIK) & ((Frege h) . (id J)) . j is non empty finite Subset of K ) ) & (Frege h) . (id J) is V9() ManySortedSet of J & (Frege h) . (id J) in Funcs (J,FIK) & (Frege h) . (id J) in Funcs (J,(Fin K)) ) )

set f = (Frege h) . (id J);

assume h in product (doms (curry H)) ; :: thesis: ( ( for j being Element of J holds

( ((Frege h) . (id J)) . j = (h . j) . j & h . j in Funcs (J,FIK) & ((Frege h) . (id J)) . j is non empty finite Subset of K ) ) & (Frege h) . (id J) is V9() ManySortedSet of J & (Frege h) . (id J) in Funcs (J,FIK) & (Frege h) . (id J) in Funcs (J,(Fin K)) )

then A21: h in dom (Frege (curry H)) by PARTFUN1:def 2;

then A22: dom h = dom (curry H) by Th8

.= J by Th20 ;

A23: for x being object st x in dom (doms h) holds

(id J) . x in (doms h) . x

then id J in product (doms h) by A22, A23, CARD_3:9;

then A24: id J in dom (Frege h) by PARTFUN1:def 2;

then A25: dom ((Frege h) . (id J)) = J by A22, Th8;

then reconsider f9 = (Frege h) . (id J) as ManySortedSet of J by PARTFUN1:def 2, RELAT_1:def 18;

thus A26: for j being Element of J holds

( ((Frege h) . (id J)) . j = (h . j) . j & h . j in Funcs (J,FIK) & ((Frege h) . (id J)) . j is non empty finite Subset of K ) :: thesis: ( (Frege h) . (id J) is V9() ManySortedSet of J & (Frege h) . (id J) in Funcs (J,FIK) & (Frege h) . (id J) in Funcs (J,(Fin K)) )

not f9 . j is empty ;

hence (Frege h) . (id J) is V9() ManySortedSet of J by PBOOLE:def 13; :: thesis: ( (Frege h) . (id J) in Funcs (J,FIK) & (Frege h) . (id J) in Funcs (J,(Fin K)) )

A30: rng ((Frege h) . (id J)) c= FIK

rng ((Frege h) . (id J)) c= Fin K by A19, A30;

hence (Frege h) . (id J) in Funcs (J,(Fin K)) by A25, FUNCT_2:def 2; :: thesis: verum

end;( ((Frege h) . (id J)) . j = (h . j) . j & h . j in Funcs (J,FIK) & ((Frege h) . (id J)) . j is non empty finite Subset of K ) ) & (Frege h) . (id J) is V9() ManySortedSet of J & (Frege h) . (id J) in Funcs (J,FIK) & (Frege h) . (id J) in Funcs (J,(Fin K)) ) )

set f = (Frege h) . (id J);

assume h in product (doms (curry H)) ; :: thesis: ( ( for j being Element of J holds

( ((Frege h) . (id J)) . j = (h . j) . j & h . j in Funcs (J,FIK) & ((Frege h) . (id J)) . j is non empty finite Subset of K ) ) & (Frege h) . (id J) is V9() ManySortedSet of J & (Frege h) . (id J) in Funcs (J,FIK) & (Frege h) . (id J) in Funcs (J,(Fin K)) )

then A21: h in dom (Frege (curry H)) by PARTFUN1:def 2;

then A22: dom h = dom (curry H) by Th8

.= J by Th20 ;

A23: for x being object st x in dom (doms h) holds

(id J) . x in (doms h) . x

proof

( dom (id J) = J & dom (doms h) = dom h )
by FUNCT_6:59;
let x be object ; :: thesis: ( x in dom (doms h) implies (id J) . x in (doms h) . x )

assume x in dom (doms h) ; :: thesis: (id J) . x in (doms h) . x

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

h . j in (J --> (Funcs (J,FIK))) . j by A21, Lm6;

then h . j in Funcs (J,FIK) ;

then ex g being Function st

( g = h . j & dom g = J & rng g c= FIK ) by FUNCT_2:def 2;

then ( (id J) . j = j & (doms h) . j = J ) by A22, FUNCT_6:22;

hence (id J) . x in (doms h) . x ; :: thesis: verum

end;assume x in dom (doms h) ; :: thesis: (id J) . x in (doms h) . x

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

h . j in (J --> (Funcs (J,FIK))) . j by A21, Lm6;

then h . j in Funcs (J,FIK) ;

then ex g being Function st

( g = h . j & dom g = J & rng g c= FIK ) by FUNCT_2:def 2;

then ( (id J) . j = j & (doms h) . j = J ) by A22, FUNCT_6:22;

hence (id J) . x in (doms h) . x ; :: thesis: verum

then id J in product (doms h) by A22, A23, CARD_3:9;

then A24: id J in dom (Frege h) by PARTFUN1:def 2;

then A25: dom ((Frege h) . (id J)) = J by A22, Th8;

then reconsider f9 = (Frege h) . (id J) as ManySortedSet of J by PARTFUN1:def 2, RELAT_1:def 18;

thus A26: for j being Element of J holds

( ((Frege h) . (id J)) . j = (h . j) . j & h . j in Funcs (J,FIK) & ((Frege h) . (id J)) . j is non empty finite Subset of K ) :: thesis: ( (Frege h) . (id J) is V9() ManySortedSet of J & (Frege h) . (id J) in Funcs (J,FIK) & (Frege h) . (id J) in Funcs (J,(Fin K)) )

proof

then
for j being object st j in J holds
let j be Element of J; :: thesis: ( ((Frege h) . (id J)) . j = (h . j) . j & h . j in Funcs (J,FIK) & ((Frege h) . (id J)) . j is non empty finite Subset of K )

thus A27: ((Frege h) . (id J)) . j = (h . j) . ((id J) . j) by A22, A24, Th9

.= (h . j) . j ; :: thesis: ( h . j in Funcs (J,FIK) & ((Frege h) . (id J)) . j is non empty finite Subset of K )

h . j in (J --> (Funcs (J,FIK))) . j by A21, Lm6;

hence h . j in Funcs (J,FIK) ; :: thesis: ((Frege h) . (id J)) . j is non empty finite Subset of K

then consider g being Function such that

A28: ( g = h . j & dom g = J ) and

A29: rng g c= FIK by FUNCT_2:def 2;

((Frege h) . (id J)) . j in rng g by A27, A28, FUNCT_1:def 3;

then ((Frege h) . (id J)) . j in FIK by A29;

then ex A being Subset of K st

( ((Frege h) . (id J)) . j = A & A is finite & A <> {} ) ;

hence ((Frege h) . (id J)) . j is non empty finite Subset of K ; :: thesis: verum

end;thus A27: ((Frege h) . (id J)) . j = (h . j) . ((id J) . j) by A22, A24, Th9

.= (h . j) . j ; :: thesis: ( h . j in Funcs (J,FIK) & ((Frege h) . (id J)) . j is non empty finite Subset of K )

h . j in (J --> (Funcs (J,FIK))) . j by A21, Lm6;

hence h . j in Funcs (J,FIK) ; :: thesis: ((Frege h) . (id J)) . j is non empty finite Subset of K

then consider g being Function such that

A28: ( g = h . j & dom g = J ) and

A29: rng g c= FIK by FUNCT_2:def 2;

((Frege h) . (id J)) . j in rng g by A27, A28, FUNCT_1:def 3;

then ((Frege h) . (id J)) . j in FIK by A29;

then ex A being Subset of K st

( ((Frege h) . (id J)) . j = A & A is finite & A <> {} ) ;

hence ((Frege h) . (id J)) . j is non empty finite Subset of K ; :: thesis: verum

not f9 . j is empty ;

hence (Frege h) . (id J) is V9() ManySortedSet of J by PBOOLE:def 13; :: thesis: ( (Frege h) . (id J) in Funcs (J,FIK) & (Frege h) . (id J) in Funcs (J,(Fin K)) )

A30: rng ((Frege h) . (id J)) c= FIK

proof

hence
(Frege h) . (id J) in Funcs (J,FIK)
by A25, FUNCT_2:def 2; :: thesis: (Frege h) . (id J) in Funcs (J,(Fin K))
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((Frege h) . (id J)) or y in FIK )

assume y in rng ((Frege h) . (id J)) ; :: thesis: y in FIK

then consider j being object such that

A31: j in dom ((Frege h) . (id J)) and

A32: y = ((Frege h) . (id J)) . j by FUNCT_1:def 3;

((Frege h) . (id J)) . j is non empty finite Subset of K by A26, A25, A31;

hence y in FIK by A32; :: thesis: verum

end;assume y in rng ((Frege h) . (id J)) ; :: thesis: y in FIK

then consider j being object such that

A31: j in dom ((Frege h) . (id J)) and

A32: y = ((Frege h) . (id J)) . j by FUNCT_1:def 3;

((Frege h) . (id J)) . j is non empty finite Subset of K by A26, A25, A31;

hence y in FIK by A32; :: thesis: verum

rng ((Frege h) . (id J)) c= Fin K by A19, A30;

hence (Frege h) . (id J) in Funcs (J,(Fin K)) by A25, FUNCT_2:def 2; :: thesis: verum

proof

rng (Infs ) is_<=_than sup X
defpred S_{1}[ object , object , object ] means $1 = F . ($3,$2);

let h be Element of product (doms (curry H)); :: thesis: Inf <= sup X

h in product (doms (curry H)) ;

then A34: h in dom (Frege (curry H)) by PARTFUN1:def 2;

for x being object st x in dom h holds

h . x is Function

reconsider f = (Frege h9) . (id J) as V9() ManySortedSet of J by A20;

A36: for j being object st j in J holds

for x being object st x in f . j holds

ex y being object st

( y in (J --> the carrier of L) . j & S_{1}[y,x,j] )

for j being object st j in J holds

ex g being Function of (f . j),((J --> the carrier of L) . j) st

( g = G . j & ( for x being object st x in f . j holds

S_{1}[g . x,x,j] ) )
from MSSUBFAM:sch 1(A36);

then consider G being ManySortedFunction of f,J --> the carrier of L such that

A38: for j being object st j in J holds

ex g being Function of (f . j),((J --> the carrier of L) . j) st

( g = G . j & ( for x being object st x in f . j holds

g . x = F . (j,x) ) ) ;

reconsider G = G as DoubleIndexedSet of f,L ;

A39: for j being Element of J

for x being object st x in f . j holds

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

then A50: Inf <= Inf by YELLOW_2:def 6;

f in Funcs (J,(Fin K)) by A20;

then Inf in X by A17, A39;

then Inf <= sup X by YELLOW_2:22;

hence Inf <= sup X by A50, ORDERS_2:3; :: thesis: verum

end;let h be Element of product (doms (curry H)); :: thesis: Inf <= sup X

h in product (doms (curry H)) ;

then A34: h in dom (Frege (curry H)) by PARTFUN1:def 2;

for x being object st x in dom h holds

h . x is Function

proof

then reconsider h9 = h as Function-yielding Function by FUNCOP_1:def 6;
let x be object ; :: thesis: ( x in dom h implies h . x is Function )

assume A35: x in dom h ; :: thesis: h . x is Function

dom h = dom (curry H) by A34, Th8

.= J by Th20 ;

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

h . j in (J --> (Funcs (J,FIK))) . j by A34, Lm6;

then h . j in Funcs (J,FIK) ;

hence h . x is Function ; :: thesis: verum

end;assume A35: x in dom h ; :: thesis: h . x is Function

dom h = dom (curry H) by A34, Th8

.= J by Th20 ;

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

h . j in (J --> (Funcs (J,FIK))) . j by A34, Lm6;

then h . j in Funcs (J,FIK) ;

hence h . x is Function ; :: thesis: verum

reconsider f = (Frege h9) . (id J) as V9() ManySortedSet of J by A20;

A36: for j being object st j in J holds

for x being object st x in f . j holds

ex y being object st

( y in (J --> the carrier of L) . j & S

proof

ex G being ManySortedFunction of f,J --> the carrier of L st
let i be object ; :: thesis: ( i in J implies for x being object st x in f . i holds

ex y being object st

( y in (J --> the carrier of L) . i & S_{1}[y,x,i] ) )

assume i in J ; :: thesis: for x being object st x in f . i holds

ex y being object st

( y in (J --> the carrier of L) . i & S_{1}[y,x,i] )

then reconsider j = i as Element of J ;

let x be object ; :: thesis: ( x in f . i implies ex y being object st

( y in (J --> the carrier of L) . i & S_{1}[y,x,i] ) )

assume A37: x in f . i ; :: thesis: ex y being object st

( y in (J --> the carrier of L) . i & S_{1}[y,x,i] )

f . j is Subset of K by A20;

then reconsider k = x as Element of K by A37;

take y = F . [j,k]; :: thesis: ( y in (J --> the carrier of L) . i & S_{1}[y,x,i] )

thus ( y in (J --> the carrier of L) . i & S_{1}[y,x,i] )
; :: thesis: verum

end;ex y being object st

( y in (J --> the carrier of L) . i & S

assume i in J ; :: thesis: for x being object st x in f . i holds

ex y being object st

( y in (J --> the carrier of L) . i & S

then reconsider j = i as Element of J ;

let x be object ; :: thesis: ( x in f . i implies ex y being object st

( y in (J --> the carrier of L) . i & S

assume A37: x in f . i ; :: thesis: ex y being object st

( y in (J --> the carrier of L) . i & S

f . j is Subset of K by A20;

then reconsider k = x as Element of K by A37;

take y = F . [j,k]; :: thesis: ( y in (J --> the carrier of L) . i & S

thus ( y in (J --> the carrier of L) . i & S

for j being object st j in J holds

ex g being Function of (f . j),((J --> the carrier of L) . j) st

( g = G . j & ( for x being object st x in f . j holds

S

then consider G being ManySortedFunction of f,J --> the carrier of L such that

A38: for j being object st j in J holds

ex g being Function of (f . j),((J --> the carrier of L) . j) st

( g = G . j & ( for x being object st x in f . j holds

g . x = F . (j,x) ) ) ;

reconsider G = G as DoubleIndexedSet of f,L ;

A39: for j being Element of J

for x being object st x in f . j holds

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

proof

Inf is_<=_than rng (Sups )
let j be Element of J; :: thesis: for x being object st x in f . j holds

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

let x be object ; :: thesis: ( x in f . j implies (G . j) . x = F . (j,x) )

assume A40: x in f . j ; :: thesis: (G . j) . x = F . (j,x)

ex g being Function of (f . j),((J --> the carrier of L) . j) st

( g = G . j & ( for x being object st x in f . j holds

g . x = F . (j,x) ) ) by A38;

hence (G . j) . x = F . (j,x) by A40; :: thesis: verum

end;(G . j) . x = F . (j,x)

let x be object ; :: thesis: ( x in f . j implies (G . j) . x = F . (j,x) )

assume A40: x in f . j ; :: thesis: (G . j) . x = F . (j,x)

ex g being Function of (f . j),((J --> the carrier of L) . j) st

( g = G . j & ( for x being object st x in f . j holds

g . x = F . (j,x) ) ) by A38;

hence (G . j) . x = F . (j,x) by A40; :: thesis: verum

proof

then
Inf <= inf (rng (Sups ))
by YELLOW_0:33;
let y be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not y in rng (Sups ) or Inf <= y )

assume y in rng (Sups ) ; :: thesis: Inf <= y

then consider j being Element of J such that

A41: y = Sup by Th14;

j in J ;

then A42: j in dom (curry H) by Th20;

A43: ((curry F) . j) .: (f . j) c= rng (G . j)

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

then A48: sup (((curry F) . j) .: (f . j)) <= Sup by YELLOW_2:def 5;

h . j in (J --> (Funcs (J,FIK))) . j by A34, Lm6;

then reconsider hj = h . j as Element of Funcs (J,FIK) ;

A49: Inf <= ((Frege (curry H)) . h) . j by YELLOW_2:53;

sup (((curry F) . j) .: (f . j)) = sup (((curry F) . j) .: (hj . j)) by A20

.= H . (j,hj) by A2

.= ((curry H) . j) . (h . j) by Th20

.= ((Frege (curry H)) . h) . j by A34, A42, Th9 ;

hence Inf <= y by A41, A48, A49, ORDERS_2:3; :: thesis: verum

end;assume y in rng (Sups ) ; :: thesis: Inf <= y

then consider j being Element of J such that

A41: y = Sup by Th14;

j in J ;

then A42: j in dom (curry H) by Th20;

A43: ((curry F) . j) .: (f . j) c= rng (G . j)

proof

( ex_sup_of ((curry F) . j) .: (f . j),L & ex_sup_of rng (G . j),L )
by YELLOW_0:17;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in ((curry F) . j) .: (f . j) or y in rng (G . j) )

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

then consider x being object such that

A44: x in dom ((curry F) . j) and

A45: x in f . j and

A46: y = ((curry F) . j) . x by FUNCT_1:def 6;

reconsider k = x as Element of K by A44;

A47: k in dom (G . j) by A45, FUNCT_2:def 1;

y = F . (j,k) by A46, Th20

.= (G . j) . k by A39, A45 ;

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

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

then consider x being object such that

A44: x in dom ((curry F) . j) and

A45: x in f . j and

A46: y = ((curry F) . j) . x by FUNCT_1:def 6;

reconsider k = x as Element of K by A44;

A47: k in dom (G . j) by A45, FUNCT_2:def 1;

y = F . (j,k) by A46, Th20

.= (G . j) . k by A39, A45 ;

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

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

then A48: sup (((curry F) . j) .: (f . j)) <= Sup by YELLOW_2:def 5;

h . j in (J --> (Funcs (J,FIK))) . j by A34, Lm6;

then reconsider hj = h . j as Element of Funcs (J,FIK) ;

A49: Inf <= ((Frege (curry H)) . h) . j by YELLOW_2:53;

sup (((curry F) . j) .: (f . j)) = sup (((curry F) . j) .: (hj . j)) by A20

.= H . (j,hj) by A2

.= ((curry H) . j) . (h . j) by Th20

.= ((Frege (curry H)) . h) . j by A34, A42, Th9 ;

hence Inf <= y by A41, A48, A49, ORDERS_2:3; :: thesis: verum

then A50: Inf <= Inf by YELLOW_2:def 6;

f in Funcs (J,(Fin K)) by A20;

then Inf in X by A17, A39;

then Inf <= sup X by YELLOW_2:22;

hence Inf <= sup X by A50, ORDERS_2:3; :: thesis: verum

proof

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

assume x in rng (Infs ) ; :: thesis: x <= sup X

then consider h being object such that

A51: h in dom (Frege (curry H)) and

A52: x = //\ (((Frege (curry H)) . h),L) by Th13;

reconsider h = h as Element of product (doms (curry H)) by A51;

Inf <= sup X by A33;

hence x <= sup X by A52; :: thesis: verum

end;assume x in rng (Infs ) ; :: thesis: x <= sup X

then consider h being object such that

A51: h in dom (Frege (curry H)) and

A52: x = //\ (((Frege (curry H)) . h),L) by Th13;

reconsider h = h as Element of product (doms (curry H)) by A51;

Inf <= sup X by A33;

hence x <= sup X by A52; :: thesis: verum

dom (curry F) = J by Th20

.= dom (curry H) by Th20 ;

then Inf = Inf by A15, Th11;

then Inf <= sup X by A14, A53, YELLOW_2:def 5;

hence Inf = sup X by A18, ORDERS_2:2; :: thesis: verum