:: deftheorem defines sum_of_squares REALALG1:def 9 :
for R being Ring
for a being Element of R holds
( a is sum_of_squares iff ex f being FinSequence of R st
( Sum f = a & ( for i being Nat st i in dom f holds
ex a being Element of R st f . i = a ^2 ) ) );