A1: Support p is finite by POLYNOM1:def 5;
card (Support p) = card (Support (p permuted_by perm)) by Th23;
then Support (p permuted_by perm) is finite by A1;
hence p permuted_by perm is finite-Support by POLYNOM1:def 5; :: thesis: verum