now :: thesis: for i being Nat st i in dom f holds
ex a being Element of F st f . i = a ^2

let i be Nat; :: thesis: ( i in dom f implies ex a being Element of F st f . i = a ^2 )
assume i in dom f ; :: thesis: ex a being Element of F st f . i = a ^2
then reconsider j = i as Element of dom f ;
f . j is square by REALALG2:def 5;
hence ex a being Element of F st f . i = a ^2 ; :: thesis: verum

end;

hence Sum f is sum_of_squares ; :: thesis: verum