theorem maina: :: REALALG3:27

for F being Field
for E being FieldExtension of F
for a being Element of E
for b being Element of F
for f being non empty quadratic FinSequence of (FAdj (F,{a})) st not a in F & a ^2 = b & Sum f in F holds
ex g1, g2 being non empty quadratic FinSequence of F st Sum f = (Sum g1) + (b * (Sum g2))