let r be Element of F_Rat; :: thesis: ( 0 <= r implies r is sum_of_squares )
assume AS: 0 <= r ; :: thesis: r is sum_of_squares
r in { r where r is Element of RAT : 0 <= r } by AS, GAUSSINT:def 14;
then r in QS F_Rat by REALALG1:38;
then ex s being Element of F_Rat st
( s = r & s is sum_of_squares ) ;
hence r is sum_of_squares ; :: thesis: verum