set f = - p;
A1: Support (- p) c= Support p

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Support (- p) or x in Support p )
assume A2: x in Support (- p) ; :: thesis: x in Support p
then reconsider x9 = x as Element of Bags n ;
(- p) . x9 <> 0. L by A2, Def4;
then - (p . x9) <> 0. L by Th17;
then p . x9 <> 0. L by RLVECT_1:12;
hence x in Support p by Def4; :: thesis: verum

end;

Support p is finite by Def5;
hence - p is finite-Support by A1; :: thesis: verum