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
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 )
assume f in Funcs J,(Fin K) ; :: thesis: for j being Element of J holds f . j is finite Subset of
then A1: ex f' being Function st
( f' = f & dom f' = J & rng f' c= Fin K ) by FUNCT_2:def 2;
for j being Element of J holds f . j is finite Subset of

proof

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

end;

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