let o be object ; :: thesis: ( o in (- P) * P implies o in - P )
assume o in (- P) * P ; :: thesis: o in - P
then consider a, b being Element of R such that
A: ( o = a * b & a in - P & b in P ) ;
- b in - P by A;
then B: a * (- b) in (- P) * (- P) by A;
(- P) * (- P) c= P by v1;
then a * (- b) in P by B;
then - (a * b) in P by VECTSP_1:8;
then - (- (a * b)) in - P ;
hence o in - P by A; :: thesis: verum