let S be Subset of R; :: thesis: ( S is with_squares & S is add-closed implies S is with_sums_of_squares )
assume AS: ( S is with_squares & S is add-closed ) ; :: thesis: S is with_sums_of_squares
defpred S₁[ Nat] means for f being FinSequence of R st len f = R & ( for i being Nat st i in dom f holds
ex x being Element of R st f . i = x ^2 ) holds
Sum f in S;

now :: thesis: for f being FinSequence of R st len f = 0 & ( for i being Nat st i in dom f holds
ex x being Element of R st f . i = x ^2 ) holds
Sum f in S

let f be FinSequence of R; :: thesis: ( len f = 0 & ( for i being Nat st i in dom f holds
ex x being Element of R st f . i = x ^2 ) implies Sum f in S )
assume ( len f = 0 & ( for i being Nat st i in dom f holds
ex x being Element of R st f . i = x ^2 ) ) ; :: thesis: Sum f in S
then f = <*> the carrier of R ;
then Sum f = 0. R by RLVECT_1:43;
then Sum f in SQ R ;
hence Sum f in S by AS; :: thesis: verum

end;

then A: S₁[ 0 ] ;

B: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume IV: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for f being FinSequence of R st len f = k + 1 & ( for i being Nat st i in dom f holds
ex x being Element of R st f . i = x ^2 ) holds
Sum f in S

let f be FinSequence of R; :: thesis: ( len f = k + 1 & ( for i being Nat st i in dom f holds
ex x being Element of R st f . i = x ^2 ) implies Sum f in S )
assume B0: ( len f = k + 1 & ( for i being Nat st i in dom f holds
ex x being Element of R st f . i = x ^2 ) ) ; :: thesis: Sum f in S
then f <> {} ;
then consider g being FinSequence, x being object such that
B1: f = g ^ <*x*> by FINSEQ_1:46;
reconsider g = g, h = <*x*> as FinSequence of R by B1, FINSEQ_1:36;
len h = 1 by FINSEQ_1:39;
then B2: len f = (len g) + 1 by B1, FINSEQ_1:22;

now :: thesis: for i being Nat st i in dom g holds
ex x being Element of R st g . i = x ^2

let i be Nat; :: thesis: ( i in dom g implies ex x being Element of R st g . i = x ^2 )
assume C1: i in dom g ; :: thesis: ex x being Element of R st g . i = x ^2
then C2: g . i = f . i by B1, FINSEQ_1:def 7;
dom g c= dom f by B1, FINSEQ_1:26;
hence ex x being Element of R st g . i = x ^2 by B0, C2, C1; :: thesis: verum

end;

then B3: Sum g in S by IV, B2, B0;
C2: dom f = Seg (k + 1) by B0, FINSEQ_1:def 3;
B4: 1 <= k + 1 by NAT_1:11;
B5: x = f . (k + 1) by B0, B2, B1, FINSEQ_1:42;
then reconsider x = x as Element of R by B4, C2, FINSEQ_1:1, FINSEQ_2:11;
consider z being Element of R such that
B6: x = z ^2 by B0, B4, B5, C2, FINSEQ_1:1;
x is square by B6;
then B7: x in SQ R ;
(Sum g) + x = (Sum g) + (Sum <*x*>) by RLVECT_1:44
.= Sum f by B1, RLVECT_1:41 ;
hence Sum f in S by B7, B3, AS; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 2(A, B);

now :: thesis: for o being object st o in QS R holds
o in S

let o be object ; :: thesis: ( o in QS R implies o in S )
assume o in QS R ; :: thesis: o in S
then consider a being Element of R such that
A: ( o = a & a is sum_of_squares ) ;
consider f being FinSequence of R such that
B: ( Sum f = o & ( for i being Nat st i in dom f holds
ex x being Element of R st f . i = x ^2 ) ) by A;
consider n being Nat such that
H: len f = n ;
thus o in S by H, B, I; :: thesis: verum

end;

hence S is with_sums_of_squares by TARSKI:def 3; :: thesis: verum