theorem lemmaA: :: REALALG3:33

for F being ordered Field
for P being Ordering of F
for E being FieldExtension of F
for a being non zero Element of E holds
( a in QS (E,P) iff ex f being non empty b₂ -quadratic FinSequence of E st
( Sum f = a & ( for i being Element of NAT st i in dom f holds
f . i <> 0. E ) ) )