theorem XYZbS3: :: REALALG3:39

for F being ordered Field
for E being FieldExtension of F
for P being Ordering of F
for a being Element of E st a ^2 in F holds
for f being non empty b₃ -quadratic FinSequence of (FAdj (F,{a})) ex g1, g2 being non empty FinSequence of (FAdj (F,{a})) st
( Sum f = (Sum g1) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum g2))) & ( for i being Element of NAT st i in dom g1 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g1 . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) ) & ( for i being Element of NAT st i in dom g2 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g2 . i = (b * c1) * c2 ) ) )