support (f | X) c= support f

proof

hence
f | X is finite-support
by PRE_POLY:def 8; :: thesis: verum
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;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