support (f | X) c= support f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (f | X) or x in support f )
assume A1: x in support (f | X) ; :: thesis: x in support f
then A2: (f | X) . x <> 0 by PRE_POLY:def 7;
support (f | X) c= dom (f | X) by PRE_POLY:37;
then f . x <> 0 by A1, A2, FUNCT_1:47;
hence x in support f by PRE_POLY:def 7; :: thesis: verum

end;

hence f | X is finite-support by PRE_POLY:def 8; :: thesis: verum