set f = <*(1. E)*>;
F is Subfield of E by FIELD_4:7;
then A: 1. E = 1. F by EC_PF_1:def 1;
B: dom <*(1. E)*> = {1} by FINSEQ_1:2, FINSEQ_1:38;

now :: thesis: for i being Element of dom <*(1. E)*> ex a being non zero Element of E ex b being Element of E st
( a in P & <*(1. E)*> . i = a * (b ^2) )

let i be Element of dom <*(1. E)*>; :: thesis: ex a being non zero Element of E ex b being Element of E st
( a in P & <*(1. E)*> . i = a * (b ^2) )
i = 1 by B, TARSKI:def 1;
then (1. E) * ((1. E) ^2) = <*(1. E)*> . i ;
hence ex a being non zero Element of E ex b being Element of E st
( a in P & <*(1. E)*> . i = a * (b ^2) ) by A, REALALG1:25; :: thesis: verum

end;

then <*(1. E)*> is P -quadratic ;
then C: Sum <*(1. E)*> in { (Sum f) where f is P -quadratic FinSequence of E : verum } ;

now :: thesis: for o being object st o in { (Sum f) where f is P -quadratic FinSequence of E : verum } holds
o in the carrier of E

let o be object ; :: thesis: ( o in { (Sum f) where f is P -quadratic FinSequence of E : verum } implies o in the carrier of E )
assume o in { (Sum f) where f is P -quadratic FinSequence of E : verum } ; :: thesis: o in the carrier of E
then consider f being P -quadratic FinSequence of E such that
D: o = Sum f ;
thus o in the carrier of E by D; :: thesis: verum

end;

then { (Sum f) where f is P -quadratic FinSequence of E : verum } c= the carrier of E ;
hence { (Sum f) where f is P -quadratic FinSequence of E : verum } is non empty Subset of E by C; :: thesis: verum