let R be Ring; :: thesis: for a being Element of R st a is square holds
a is sum_of_squares
let a be Element of R; :: thesis: ( a is square implies a is sum_of_squares )
assume AS: a is square ; :: thesis: a is sum_of_squares
set f = <*a*>;
A: Sum <*a*> = a by RLVECT_1:44;
now :: thesis: for i being Nat st i in dom <*a*> holds
ex b being Element of R st <*a*> . i = b ^2
let i be Nat; :: thesis: ( i in dom <*a*> implies ex b being Element of R st <*a*> . i = b ^2 )
assume i in dom <*a*> ; :: thesis: ex b being Element of R st <*a*> . i = b ^2
then i in {1} by FINSEQ_1:2, FINSEQ_1:38;
then i = 1 by TARSKI:def 1;
hence ex b being Element of R st <*a*> . i = b ^2 by AS, FINSEQ_1:40; :: thesis: verum
end;
hence a is sum_of_squares by A; :: thesis: verum