let f be Function; :: thesis: ( f is finite implies f is finite-support )
assume f is finite ; :: thesis: f is finite-support
then dom f is finite ;
hence support f is finite by Th36, FINSET_1:1; :: according to PRE_POLY:def 8 :: thesis: verum