let J, K be non empty set ; :: thesis: for f being Function st f in Funcs (J,(Fin K)) holds
for j being Element of J holds f . j is finite Subset of K
let f be Function; :: thesis: ( f in Funcs (J,(Fin K)) implies for j being Element of J holds f . j is finite Subset of K )
assume f in Funcs (J,(Fin K)) ; :: thesis: for j being Element of J holds f . j is finite Subset of K
then A1: ex f9 being Function st
( f9 = f & dom f9 = J & rng f9 c= Fin K ) by FUNCT_2:def 2;
for j being Element of J holds f . j is finite Subset of K

proof

let j be Element of J; :: thesis: f . j is finite Subset of K
f . j in rng f by A1, FUNCT_1:def 3;
hence f . j is finite Subset of K by A1, FINSUB_1:def 5; :: thesis: verum

end;

hence for j being Element of J holds f . j is finite Subset of K ; :: thesis: verum