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

for j being Element of J

for F being Function of [:J,K:],D

for f being V9() ManySortedSet of J st f in Funcs (J,(Fin K)) holds

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

rng (G . j) is finite Subset of (rng ((curry F) . j))

let J, K, D be non empty set ; :: thesis: for j being Element of J

for F being Function of [:J,K:],D

for f being V9() ManySortedSet of J st f in Funcs (J,(Fin K)) holds

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

rng (G . j) is finite Subset of (rng ((curry F) . j))

let j be Element of J; :: thesis: for F being Function of [:J,K:],D

for f being V9() ManySortedSet of J st f in Funcs (J,(Fin K)) holds

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

rng (G . j) is finite Subset of (rng ((curry F) . j))

let F be Function of [:J,K:],D; :: thesis: for f being V9() ManySortedSet of J st f in Funcs (J,(Fin K)) holds

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

rng (G . j) is finite Subset of (rng ((curry F) . j))

let f be V9() ManySortedSet of J; :: thesis: ( f in Funcs (J,(Fin K)) implies for 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) ) holds

rng (G . j) is finite Subset of (rng ((curry F) . j)) )

assume f in Funcs (J,(Fin K)) ; :: thesis: for 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) ) holds

rng (G . j) is finite Subset of (rng ((curry F) . j))

then A1: f . j is finite Subset of K by Lm11;

let G be DoubleIndexedSet of f,L; :: thesis: ( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) implies rng (G . j) is finite Subset of (rng ((curry F) . j)) )

assume A2: for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ; :: thesis: rng (G . j) is finite Subset of (rng ((curry F) . j))

rng (G . j) c= rng ((curry F) . j)

for j being Element of J

for F being Function of [:J,K:],D

for f being V9() ManySortedSet of J st f in Funcs (J,(Fin K)) holds

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

rng (G . j) is finite Subset of (rng ((curry F) . j))

let J, K, D be non empty set ; :: thesis: for j being Element of J

for F being Function of [:J,K:],D

for f being V9() ManySortedSet of J st f in Funcs (J,(Fin K)) holds

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

rng (G . j) is finite Subset of (rng ((curry F) . j))

let j be Element of J; :: thesis: for F being Function of [:J,K:],D

for f being V9() ManySortedSet of J st f in Funcs (J,(Fin K)) holds

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

rng (G . j) is finite Subset of (rng ((curry F) . j))

let F be Function of [:J,K:],D; :: thesis: for f being V9() ManySortedSet of J st f in Funcs (J,(Fin K)) holds

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

rng (G . j) is finite Subset of (rng ((curry F) . j))

let f be V9() ManySortedSet of J; :: thesis: ( f in Funcs (J,(Fin K)) implies for 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) ) holds

rng (G . j) is finite Subset of (rng ((curry F) . j)) )

assume f in Funcs (J,(Fin K)) ; :: thesis: for 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) ) holds

rng (G . j) is finite Subset of (rng ((curry F) . j))

then A1: f . j is finite Subset of K by Lm11;

let G be DoubleIndexedSet of f,L; :: thesis: ( ( for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ) implies rng (G . j) is finite Subset of (rng ((curry F) . j)) )

assume A2: for j being Element of J

for x being object st x in f . j holds

(G . j) . x = F . (j,x) ; :: thesis: rng (G . j) is finite Subset of (rng ((curry F) . j))

rng (G . j) c= rng ((curry F) . j)

proof

hence
rng (G . j) is finite Subset of (rng ((curry F) . j))
by A1; :: thesis: verum
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (G . j) or y in rng ((curry F) . j) )

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

then consider k being object such that

A3: k in dom (G . j) and

A4: y = (G . j) . k by FUNCT_1:def 3;

A5: k in f . j by A3;

then A6: k in K by A1;

reconsider k = k as Element of K by A1, A5;

A7: k in dom ((curry F) . j) by A6, Th20;

y = F . (j,k) by A2, A3, A4

.= ((curry F) . j) . k by Th20 ;

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

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

then consider k being object such that

A3: k in dom (G . j) and

A4: y = (G . j) . k by FUNCT_1:def 3;

A5: k in f . j by A3;

then A6: k in K by A1;

reconsider k = k as Element of K by A1, A5;

A7: k in dom ((curry F) . j) by A6, Th20;

y = F . (j,k) by A2, A3, A4

.= ((curry F) . j) . k by Th20 ;

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