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 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 set st x in f . j holds
(G . j) . x = F . j,x ) holds
rng (G . j) is finite Subset of
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 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 set st x in f . j holds
(G . j) . x = F . j,x ) holds
rng (G . j) is finite Subset of
let j be Element of J; :: thesis: for F being Function of [:J,K:],D
for f being V9() ManySortedSet of 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 set st x in f . j holds
(G . j) . x = F . j,x ) holds
rng (G . j) is finite Subset of
let F be Function of [:J,K:],D; :: thesis: for f being V9() ManySortedSet of 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 set st x in f . j holds
(G . j) . x = F . j,x ) holds
rng (G . j) is finite Subset of
let f be V9() ManySortedSet of ; :: 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 set st x in f . j holds
(G . j) . x = F . j,x ) holds
rng (G . j) is finite Subset of )
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 set st x in f . j holds
(G . j) . x = F . j,x ) holds
rng (G . j) is finite Subset of
then A1: f . j is finite Subset of by Lm11;
let G be DoubleIndexedSet of f,L; :: thesis: ( ( for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . j,x ) implies rng (G . j) is finite Subset of )
assume A2: for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . j,x ; :: thesis: rng (G . j) is finite Subset of
rng (G . j) c= rng ((curry F) . j)

proof

let y be set ; :: 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 set such that
A3: k in dom (G . j) and
A4: y = (G . j) . k by FUNCT_1:def 5;
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 5; :: thesis: verum

end;

hence rng (G . j) is finite Subset of by A1; :: thesis: verum