let F be Field; :: thesis: 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))
let E be FieldExtension of F; :: thesis: 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))
let a be Element of E; :: thesis: 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))
let b be Element of F; :: thesis: 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))
let f be non empty quadratic FinSequence of (FAdj (F,{a})); :: thesis: ( not a in F & a ^2 = b & Sum f in F implies ex g1, g2 being non empty quadratic FinSequence of F st Sum f = (Sum g1) + (b * (Sum g2)) )
assume AS: ( not a in F & a ^2 = b & Sum f in F ) ; :: thesis: ex g1, g2 being non empty quadratic FinSequence of F st Sum f = (Sum g1) + (b * (Sum g2))
then AS1: ( not a in F & a ^2 in F ) ;
set K = FAdj (F,{a});
H0: ( F is Subring of FAdj (F,{a}) & FAdj (F,{a}) is Subring of E & F is Subring of E ) by FIELD_4:def 1, FIELD_5:12;
( {a} is Subset of (FAdj (F,{a})) & a in {a} ) by TARSKI:def 1, FIELD_6:35;
then a is FAdj (F,{a}) -membered ;
then reconsider a = a as FAdj (F,{a}) -membered Element of E ;
reconsider Sf = Sum f as Element of F by AS;
consider g1, g2 being non empty quadratic FinSequence of F, g3 being non empty FinSequence of F such that
A: Sum f = (@ (((Sum g1) + (b * (Sum g2))),(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ ((Sum g3),(FAdj (F,{a}))))) by AS, mainY;
B: Sum f = (@ (Sf,(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (0. (FAdj (F,{a})))) by FIELD_7:def 4;
@ (((Sum g1) + (b * (Sum g2))),(FAdj (F,{a}))) = Sum f

proof

D: ( @ (Sf,(FAdj (F,{a}))) = Sf & 0. (FAdj (F,{a})) = 0. F & (Sum g1) + (b * (Sum g2)) = @ (((Sum g1) + (b * (Sum g2))),(FAdj (F,{a}))) & @ ((Sum g3),(FAdj (F,{a}))) = Sum g3 ) by H0, C0SP1:def 3, FIELD_7:def 4;
then ( @ (((Sum g1) + (b * (Sum g2))),(FAdj (F,{a}))) in F & Sum g3 in F & @ (Sf,(FAdj (F,{a}))) in F & 0. (FAdj (F,{a})) in F ) ;
hence @ (((Sum g1) + (b * (Sum g2))),(FAdj (F,{a}))) = Sum f by B, D, AS1, A, XYZc; :: thesis: verum

end;

hence ex g1, g2 being non empty quadratic FinSequence of F st Sum f = (Sum g1) + (b * (Sum g2)) by FIELD_7:def 4; :: thesis: verum