let x, y be Element of R; :: according to REALALG1:def 5 :: thesis: ( x in QS R & y in QS R implies x * y in QS R )
assume AS: ( x in QS R & y in QS R ) ; :: thesis: x * y in QS R
then consider a being Element of R such that
A: ( x = a & a is sum_of_squares ) ;
consider b being Element of R such that
B: ( y = b & b is sum_of_squares ) by AS;
thus x * y in QS R by A, B; :: thesis: verum