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)
proof
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;
hence rng (G . j) is finite Subset of (rng ((curry F) . j)) by A1; :: thesis: verum