theorem mainY: :: REALALG3:26

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 holds
ex g1, g2 being non empty quadratic FinSequence of F ex g3 being non empty FinSequence of F st Sum f = (@ (((Sum g1) + (b * (Sum g2))),(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ ((Sum g3),(FAdj (F,{a})))))