let F be Field; :: thesis: for E being FieldExtension of F
for a being Element of E st a ^2 in F holds
for b being Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in F & c2 in F & b = c1 + ((@ ((FAdj (F,{a})),a)) * c2) )
let E be FieldExtension of F; :: thesis: for a being Element of E st a ^2 in F holds
for b being Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in F & c2 in F & b = c1 + ((@ ((FAdj (F,{a})),a)) * c2) )
let a be Element of E; :: thesis: ( a ^2 in F implies for b being Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in F & c2 in F & b = c1 + ((@ ((FAdj (F,{a})),a)) * c2) ) )
assume AS: a ^2 in F ; :: thesis: for b being Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in F & c2 in F & b = c1 + ((@ ((FAdj (F,{a})),a)) * c2) )
let b be Element of (FAdj (F,{a})); :: thesis: ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in F & c2 in F & b = c1 + ((@ ((FAdj (F,{a})),a)) * c2) )
A2: ( 0. E = 0. (FAdj (F,{a})) & 1. E = 1. (FAdj (F,{a})) ) by FIELD_6:def 6;
A9: ( {a} is Subset of (FAdj (F,{a})) & a in {a} ) by TARSKI:def 1, FIELD_6:35;

per cases ( a in F or not a in F ) ;

suppose a in F ; :: thesis: ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in F & c2 in F & b = c1 + ((@ ((FAdj (F,{a})),a)) * c2) )

then {a} c= the carrier of F by TARSKI:def 1;
then A1: FAdj (F,{a}) == F by FIELD_7:3;
take b ; :: thesis: ex c2 being Element of (FAdj (F,{a})) st
( b in F & c2 in F & b = b + ((@ ((FAdj (F,{a})),a)) * c2) )
take 0. (FAdj (F,{a})) ; :: thesis: ( b in F & 0. (FAdj (F,{a})) in F & b = b + ((@ ((FAdj (F,{a})),a)) * (0. (FAdj (F,{a})))) )
thus ( b in F & 0. (FAdj (F,{a})) in F & b = b + ((@ ((FAdj (F,{a})),a)) * (0. (FAdj (F,{a})))) ) by A1; :: thesis: verum

end;

suppose A0: not a in F ; :: thesis: ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in F & c2 in F & b = c1 + ((@ ((FAdj (F,{a})),a)) * c2) )

set K = FAdj (F,{a});
set aK = @ ((FAdj (F,{a})),a);
reconsider 1V = 1. E, aV = a, bV = b as Element of (VecSp ((FAdj (F,{a})),F)) by A9, A2, FIELD_4:def 6;
{(1. E),a} is Basis of (VecSp ((FAdj (F,{a})),F)) by A0, AS, ThBas;
then Lin {1V,aV} = ModuleStr(# the carrier of (VecSp ((FAdj (F,{a})),F)), the addF of (VecSp ((FAdj (F,{a})),F)), the ZeroF of (VecSp ((FAdj (F,{a})),F)), the lmult of (VecSp ((FAdj (F,{a})),F)) #) by VECTSP_7:def 3;
then bV in Lin {1V,aV} ;
then consider l being Linear_Combination of {1V,aV} such that
A1: bV = Sum l by VECTSP_7:7;
H: ( F is Subfield of FAdj (F,{a}) & F is Subfield of E ) by FIELD_4:7;
then ( 1. E = 1. F & 1. F = 1. (FAdj (F,{a})) ) by EC_PF_1:def 1;
then A3: 1V <> aV by A0;
( {a} is Subset of (FAdj (F,{a})) & a in {a} ) by TARSKI:def 1, FIELD_6:35;
then J: a is FAdj (F,{a}) -membered ;
the carrier of F c= the carrier of (FAdj (F,{a})) by H, EC_PF_1:def 1;
then reconsider b1 = l . 1V, b2 = l . aV as Element of (FAdj (F,{a})) ;
take b1 ; :: thesis: ex c2 being Element of (FAdj (F,{a})) st
( b1 in F & c2 in F & b = b1 + ((@ ((FAdj (F,{a})),a)) * c2) )
take b2 ; :: thesis: ( b1 in F & b2 in F & b = b1 + ((@ ((FAdj (F,{a})),a)) * b2) )
A7: [(l . 1V),1V] in [: the carrier of F, the carrier of (FAdj (F,{a})):] by A2, ZFMISC_1:def 2;
A8: ( the addF of E || the carrier of (FAdj (F,{a})) = the addF of (FAdj (F,{a})) & the multF of E || the carrier of (FAdj (F,{a})) = the multF of (FAdj (F,{a})) ) by EC_PF_1:def 1;
A4: the lmult of (VecSp ((FAdj (F,{a})),F)) . ((l . 1V),1V) = ( the multF of (FAdj (F,{a})) | [: the carrier of F, the carrier of (FAdj (F,{a})):]) . (b1,(1. E)) by FIELD_4:def 6
.= the multF of (FAdj (F,{a})) . (b1,(1. E)) by A7, FUNCT_1:49
.= ( the multF of E || (carrierFA {a})) . (b1,(1. E)) by FIELD_6:def 6
.= ( the multF of E || the carrier of (FAdj (F,{a}))) . (b1,(1. E)) by FIELD_6:def 6
.= b1 * (1. (FAdj (F,{a}))) by A8, EC_PF_1:def 1 ;
A7: [(l . aV),a] in [: the carrier of F, the carrier of (FAdj (F,{a})):] by A9, ZFMISC_1:def 2;
A6: the lmult of (VecSp ((FAdj (F,{a})),F)) . ((l . aV),aV) = ( the multF of (FAdj (F,{a})) | [: the carrier of F, the carrier of (FAdj (F,{a})):]) . (b2,a) by FIELD_4:def 6
.= b2 * (@ ((FAdj (F,{a})),a)) by J, A7, FUNCT_1:49 ;
bV = ((l . 1V) * 1V) + ((l . aV) * aV) by A1, A3, VECTSP_6:18
.= b1 + ((@ ((FAdj (F,{a})),a)) * b2) by A4, A6, FIELD_4:def 6 ;
hence ( b1 in F & b2 in F & b = b1 + ((@ ((FAdj (F,{a})),a)) * b2) ) ; :: thesis: verum

end;

end;