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 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})))))
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 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})))))
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 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})))))
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 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})))))
let f be non empty quadratic FinSequence of (FAdj (F,{a})); :: thesis: ( not a in F & a ^2 = b implies 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}))))) )
assume AS: ( not a in F & a ^2 = b ) ; :: thesis: 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})))))
then ( not a in F & a ^2 in F ) ;
then consider g1, g2, g3 being non empty FinSequence of (FAdj (F,{a})) such that
A: ( g1 is non empty quadratic FinSequence of F & g2 is non empty quadratic FinSequence of F & g3 is non empty FinSequence of F & Sum f = ((Sum g1) + (((@ ((FAdj (F,{a})),a)) ^2) * (Sum g2))) + ((@ ((FAdj (F,{a})),a)) * (Sum g3)) ) by mainX;
reconsider h1 = g1, h2 = g2 as non empty quadratic FinSequence of F by A;
reconsider h3 = g3 as non empty FinSequence of F by A;
set K = FAdj (F,{a});
( {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 ;
take h1 ; :: thesis: ex g2 being non empty quadratic FinSequence of F ex g3 being non empty FinSequence of F st Sum f = (@ (((Sum h1) + (b * (Sum g2))),(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ ((Sum g3),(FAdj (F,{a})))))
take h2 ; :: thesis: ex g3 being non empty FinSequence of F st Sum f = (@ (((Sum h1) + (b * (Sum h2))),(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ ((Sum g3),(FAdj (F,{a})))))
take h3 ; :: thesis: Sum f = (@ (((Sum h1) + (b * (Sum h2))),(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ ((Sum h3),(FAdj (F,{a})))))
H: FAdj (F,{a}) is Subring of E by FIELD_5:12;
F is Subfield of FAdj (F,{a}) by FIELD_4:7;
then I: F is Subring of FAdj (F,{a}) by FIELD_5:12;
then B: ( Sum g1 = Sum h1 & Sum g2 = Sum h2 & Sum g3 = Sum h3 ) by FIELD_4:2;
D: (@ ((FAdj (F,{a})),a)) * (@ ((FAdj (F,{a})),a)) = b by AS, H, FIELD_6:16;
F: (@ ((FAdj (F,{a})),a)) * (Sum g3) = (@ ((FAdj (F,{a})),a)) * (@ ((Sum h3),(FAdj (F,{a})))) by B, FIELD_7:def 4;
((@ ((FAdj (F,{a})),a)) ^2) * (Sum g2) = b * (Sum h2) by B, D, I, FIELD_6:16;
then (Sum g1) + (((@ ((FAdj (F,{a})),a)) ^2) * (Sum g2)) = (Sum h1) + (b * (Sum h2)) by B, I, FIELD_6:15;
hence Sum f = (@ (((Sum h1) + (b * (Sum h2))),(FAdj (F,{a})))) + ((@ ((FAdj (F,{a})),a)) * (@ ((Sum h3),(FAdj (F,{a}))))) by F, A, FIELD_7:def 4; :: thesis: verum