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 Th41, FINSET_1:13; :: according to PRE_POLY:def 8 :: thesis: verum