set S = P \ {(0. R)};
A: P * P c= P by REALALG1:def 14;

now :: thesis: for s1, s2 being Element of R st s1 in P \ {(0. R)} & s2 in P \ {(0. R)} holds
s1 * s2 in P \ {(0. R)}

let s1, s2 be Element of R; :: thesis: ( s1 in P \ {(0. R)} & s2 in P \ {(0. R)} implies s1 * s2 in P \ {(0. R)} )
assume ( s1 in P \ {(0. R)} & s2 in P \ {(0. R)} ) ; :: thesis: s1 * s2 in P \ {(0. R)}
then C: ( s1 in P & not s1 in {(0. R)} & s2 in P & not s2 in {(0. R)} ) by XBOOLE_0:def 5;
then B: s1 * s2 in P * P ;

now :: thesis: not s1 * s2 in {(0. R)}

assume s1 * s2 in {(0. R)} ; :: thesis: contradiction
then s1 * s2 = 0. R by TARSKI:def 1;
then ( s1 = 0. R or s2 = 0. R ) by VECTSP_2:def 1;
hence contradiction by C, TARSKI:def 1; :: thesis: verum

end;

hence s1 * s2 in P \ {(0. R)} by A, B, XBOOLE_0:def 5; :: thesis: verum

end;

hence P ^+ is mult-closed ; :: thesis: verum