let R be Ring; :: thesis: for S being Subring of R holds QS S c= QS R
let S be Subring of R; :: thesis: QS S c= QS R
AS4: the carrier of S c= the carrier of R by C0SP1:def 3;
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in QS S or o in QS R )
assume o in QS S ; :: thesis: o in QS R
then consider a being Element of S such that
D2: ( a = o & a is sum_of_squares ) ;
consider f being FinSequence of S such that
D3: ( Sum f = a & ( for i being Nat st i in dom f holds
ex a being Element of S st f . i = a ^2 ) ) by D2;
reconsider a1 = a as Element of R by AS4;
rng f c= the carrier of R by AS4;
then reconsider g = f as FinSequence of R by FINSEQ_1:def 4;
D9: Sum g = Sum f by lemsum;

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

let i be Nat; :: thesis: ( i in dom g implies ex a being Element of R st g . i = a ^2 )
assume i in dom g ; :: thesis: ex a being Element of R st g . i = a ^2
then consider a being Element of S such that
E1: f . i = a ^2 by D3;
reconsider a1 = a as Element of R by AS4;
dom the multF of S = [: the carrier of S, the carrier of S:] by FUNCT_2:def 1;
then B6: [a,a] in dom the multF of S ;
a1 ^2 = ( the multF of R || the carrier of S) . (a,a) by B6, FUNCT_1:49
.= a ^2 by C0SP1:def 3 ;
hence ex a being Element of R st g . i = a ^2 by E1; :: thesis: verum

end;

then a1 is sum_of_squares by D3, D9;
hence o in QS R by D2; :: thesis: verum