reconsider f = <*(1. E)*> as non empty FinSequence of E ;
take f ; :: thesis: ( f is P -quadratic & not f is empty )
F is Subfield of E by FIELD_4:7;
then A: 1. E = 1. F by EC_PF_1:def 1;
B: dom f = {1} by FINSEQ_1:2, FINSEQ_1:38;

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

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

end;

hence ( f is P -quadratic & not f is empty ) ; :: thesis: verum