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

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

hence
for j being Element of J holds f . j is finite Subset of K
; :: thesis: verum
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;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