support f is finite ;
hence support ((EmptyBag X) +* f) is finite by Th12; :: according to PRE_POLY:def 8 :: thesis: verum