set T = QS (E,P);
I: F is Subfield of E by FIELD_4:7;

now :: thesis: for x, y being Element of E st x in QS (E,P) & y in QS (E,P) holds
x + y in QS (E,P)

let x, y be Element of E; :: thesis: ( x in QS (E,P) & y in QS (E,P) implies x + y in QS (E,P) )
assume AS: ( x in QS (E,P) & y in QS (E,P) ) ; :: thesis: x + y in QS (E,P)
then consider f being P -quadratic FinSequence of E such that
A: Sum f = x ;
consider g being P -quadratic FinSequence of E such that
B: Sum g = y by AS;
Sum (f ^ g) = x + y by A, B, RLVECT_1:41;
hence x + y in QS (E,P) ; :: thesis: verum

end;

hence QS (E,P) is add-closed ; :: thesis: ( QS (E,P) is mult-closed & QS (E,P) is with_sums_of_squares )

now :: thesis: for x, y being Element of E st x in QS (E,P) & y in QS (E,P) holds
x * y in QS (E,P)

let x, y be Element of E; :: thesis: ( x in QS (E,P) & y in QS (E,P) implies x * y in QS (E,P) )
assume AS: ( x in QS (E,P) & y in QS (E,P) ) ; :: thesis: x * y in QS (E,P)
then consider f being P -quadratic FinSequence of E such that
A: Sum f = x ;
consider g being P -quadratic FinSequence of E such that
B: Sum g = y by AS;
thus x * y in QS (E,P) by AS, A, B, S0; :: thesis: verum

end;

hence QS (E,P) is mult-closed ; :: thesis: QS (E,P) is with_sums_of_squares

now :: thesis: for o being object st o in QS E holds
o in QS (E,P)

let o be object ; :: thesis: ( o in QS E implies o in QS (E,P) )
assume o in QS E ; :: thesis: o in QS (E,P)
then consider a being Element of E such that
A: ( o = a & a is sum_of_squares ) ;
consider f being FinSequence of E such that
B: ( Sum f = a & ( for i being Nat st i in dom f holds
ex x being Element of E st f . i = x ^2 ) ) by A;
f is P -quadratic

proof

now :: thesis: for i being Element of NAT st i in dom f holds
ex c being non zero Element of E ex b being Element of E st
( c in P & f . i = c * (b ^2) )

let i be Element of NAT ; :: thesis: ( i in dom f implies ex c being non zero Element of E ex b being Element of E st
( c in P & f . i = c * (b ^2) ) )
assume AS: i in dom f ; :: thesis: ex c being non zero Element of E ex b being Element of E st
( c in P & f . i = c * (b ^2) )
D: 1. F = 1. E by I, EC_PF_1:def 1;
thus ex c being non zero Element of E ex b being Element of E st
( c in P & f . i = c * (b ^2) ) :: thesis: verum

proof

consider x being Element of E such that
E: f . i = x ^2 by AS, B;
f . i = (1. E) * (x ^2) by E;
hence ex c being non zero Element of E ex b being Element of E st
( c in P & f . i = c * (b ^2) ) by D, REALALG1:25; :: thesis: verum

end;

end;

hence f is P -quadratic ; :: thesis: verum

end;

hence o in QS (E,P) by A, B; :: thesis: verum

end;

then QS E c= QS (E,P) ;
hence QS (E,P) is with_sums_of_squares ; :: thesis: verum