for F being Field holds
( F is formally_real iff for f being non empty quadratic FinSequence of F st Sum f = 0. F holds
f is trivial )