theorem XYZbS3a: :: REALALG3:32

for F being ordered Field
for E being FieldExtension of F
for P being Ordering of F
for f being b₃ -quadratic FinSequence of E
for g1, g2 being FinSequence of E st f = g1 ^ g2 holds
( g1 is P -quadratic & g2 is P -quadratic )