let F be ordered Field; :: thesis: 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 )
let E be FieldExtension of F; :: thesis: 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 )
let P be Ordering of F; :: thesis: for f being P -quadratic FinSequence of E
for g1, g2 being FinSequence of E st f = g1 ^ g2 holds
( g1 is P -quadratic & g2 is P -quadratic )
let f be P -quadratic FinSequence of E; :: thesis: for g1, g2 being FinSequence of E st f = g1 ^ g2 holds
( g1 is P -quadratic & g2 is P -quadratic )
let g1, g2 be FinSequence of E; :: thesis: ( f = g1 ^ g2 implies ( g1 is P -quadratic & g2 is P -quadratic ) )
assume AS: f = g1 ^ g2 ; :: thesis: ( g1 is P -quadratic & g2 is P -quadratic )

now :: thesis: for i being Nat st i in dom g1 holds
ex a being non zero Element of E ex b being Element of E st
( a in P & g1 . i = a * (b ^2) )

let i be Nat; :: thesis: ( i in dom g1 implies ex a being non zero Element of E ex b being Element of E st
( a in P & g1 . i = a * (b ^2) ) )
assume F0: i in dom g1 ; :: thesis: ex a being non zero Element of E ex b being Element of E st
( a in P & g1 . i = a * (b ^2) )
then F1: g1 . i = f . i by AS, FINSEQ_1:def 7;
dom g1 c= dom f by AS, FINSEQ_1:26;
hence ex a being non zero Element of E ex b being Element of E st
( a in P & g1 . i = a * (b ^2) ) by F1, F0, dq; :: thesis: verum

end;

hence g1 is P -quadratic ; :: thesis: g2 is P -quadratic

now :: thesis: for i being Nat st i in dom g2 holds
ex a being non zero Element of E ex b being Element of E st
( a in P & g2 . i = a * (b ^2) )

let i be Nat; :: thesis: ( i in dom g2 implies ex a being non zero Element of E ex b being Element of E st
( a in P & g2 . i = a * (b ^2) ) )
assume F0: i in dom g2 ; :: thesis: ex a being non zero Element of E ex b being Element of E st
( a in P & g2 . i = a * (b ^2) )
then F1: g2 . i = f . ((len g1) + i) by AS, FINSEQ_1:def 7;
(len g1) + i in dom f by F0, AS, FINSEQ_1:28;
hence ex a being non zero Element of E ex b being Element of E st
( a in P & g2 . i = a * (b ^2) ) by F1, dq; :: thesis: verum

end;

hence g2 is P -quadratic ; :: thesis: verum