set f = - p;
A1: Support p is finite by Def10;
Support (- p) c= Support p

proof

let x be set ; :: 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 x' = x as Element of Bags n ;
(- p) . x' <> 0. L by A2, Def9;
then - (p . x') <> 0. L by Def22;
then p . x' <> 0. L by RLVECT_1:25;
hence x in Support p by Def9; :: thesis: verum

end;

then Support (- p) is finite by A1;
hence - p is finite-Support by Def10; :: thesis: verum