support (F * f) c= (f ") .: (support F)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in support (F * f) or y in (f ") .: (support F) )
A1: rng f = dom (f ") by FUNCT_1:33;
assume y in support (F * f) ; :: thesis: y in (f ") .: (support F)
then A2: (F * f) . y <> 0 by PRE_POLY:def 7;
then y in dom (F * f) by FUNCT_1:def 2;
then ( (F * f) . y = F . (f . y) & y in dom f & f . y in dom F ) by FUNCT_1:11, FUNCT_1:12;
then ( (f ") . (f . y) = y & f . y in support F & f . y in rng f ) by A2, PRE_POLY:def 7, FUNCT_1:34, FUNCT_1:def 3;
hence y in (f ") .: (support F) by A1, FUNCT_1:def 6; :: thesis: verum

end;

hence F * f is finite-support by PRE_POLY:def 8; :: thesis: verum