let F be ordered Field; :: thesis: for E being FieldExtension of F
for P being Ordering of F
for a being Element of E st a ^2 in F holds
for f being non empty b₂ -quadratic FinSequence of (FAdj (F,{a})) ex g1, g2 being non empty FinSequence of (FAdj (F,{a})) st
( Sum f = (Sum g1) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum g2))) & ( for i being Element of NAT st i in dom g1 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g1 . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) ) & ( for i being Element of NAT st i in dom g2 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g2 . i = (b * c1) * c2 ) ) )
let E be FieldExtension of F; :: thesis: for P being Ordering of F
for a being Element of E st a ^2 in F holds
for f being non empty b₁ -quadratic FinSequence of (FAdj (F,{a})) ex g1, g2 being non empty FinSequence of (FAdj (F,{a})) st
( Sum f = (Sum g1) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum g2))) & ( for i being Element of NAT st i in dom g1 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g1 . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) ) & ( for i being Element of NAT st i in dom g2 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g2 . i = (b * c1) * c2 ) ) )
let P be Ordering of F; :: thesis: for a being Element of E st a ^2 in F holds
for f being non empty P -quadratic FinSequence of (FAdj (F,{a})) ex g1, g2 being non empty FinSequence of (FAdj (F,{a})) st
( Sum f = (Sum g1) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum g2))) & ( for i being Element of NAT st i in dom g1 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g1 . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) ) & ( for i being Element of NAT st i in dom g2 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g2 . i = (b * c1) * c2 ) ) )
let a be Element of E; :: thesis: ( a ^2 in F implies for f being non empty P -quadratic FinSequence of (FAdj (F,{a})) ex g1, g2 being non empty FinSequence of (FAdj (F,{a})) st
( Sum f = (Sum g1) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum g2))) & ( for i being Element of NAT st i in dom g1 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g1 . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) ) & ( for i being Element of NAT st i in dom g2 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g2 . i = (b * c1) * c2 ) ) ) )
assume AA: a ^2 in F ; :: thesis: for f being non empty P -quadratic FinSequence of (FAdj (F,{a})) ex g1, g2 being non empty FinSequence of (FAdj (F,{a})) st
( Sum f = (Sum g1) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum g2))) & ( for i being Element of NAT st i in dom g1 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g1 . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) ) & ( for i being Element of NAT st i in dom g2 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g2 . i = (b * c1) * c2 ) ) )
let f be non empty P -quadratic FinSequence of (FAdj (F,{a})); :: thesis: ex g1, g2 being non empty FinSequence of (FAdj (F,{a})) st
( Sum f = (Sum g1) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum g2))) & ( for i being Element of NAT st i in dom g1 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g1 . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) ) & ( for i being Element of NAT st i in dom g2 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g2 . i = (b * c1) * c2 ) ) )
set K = FAdj (F,{a});
defpred S₁[ Nat] means for f being non empty P -quadratic FinSequence of (FAdj (F,{a})) st len f = $1 holds
ex g1, g2 being non empty FinSequence of (FAdj (F,{a})) st
( Sum f = (Sum g1) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum g2))) & ( for i being Element of NAT st i in dom g1 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g1 . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) ) & ( for i being Element of NAT st i in dom g2 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g2 . i = (b * c1) * c2 ) ) );

II: now :: thesis: for f being non empty P -quadratic FinSequence of (FAdj (F,{a})) st len f = 1 holds
ex g1, g2 being non empty FinSequence of (FAdj (F,{a})) st
( Sum f = (Sum g1) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum g2))) & ( for i being Element of NAT st i in dom g1 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g1 . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) ) & ( for i being Element of NAT st i in dom g2 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g2 . i = (b * c1) * c2 ) ) )

let f be non empty P -quadratic FinSequence of (FAdj (F,{a})); :: thesis: ( len f = 1 implies ex g1, g2 being non empty FinSequence of (FAdj (F,{a})) st
( Sum f = (Sum g1) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum g2))) & ( for i being Element of NAT st i in dom g1 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g1 . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) ) & ( for i being Element of NAT st i in dom g2 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g2 . i = (b * c1) * c2 ) ) ) )
assume len f = 1 ; :: thesis: ex g1, g2 being non empty FinSequence of (FAdj (F,{a})) st
( Sum f = (Sum g1) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum g2))) & ( for i being Element of NAT st i in dom g1 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g1 . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) ) & ( for i being Element of NAT st i in dom g2 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g2 . i = (b * c1) * c2 ) ) )
then H: f = <*(f . 1)*> by FINSEQ_1:40;
then dom f = {1} by FINSEQ_1:38, FINSEQ_1:2;
then 1 in dom f by TARSKI:def 1;
then consider d being non zero Element of (FAdj (F,{a})), b being Element of (FAdj (F,{a})) such that
A: ( d in P & f . 1 = d * (b ^2) ) by dq;
consider c1, c2 being Element of (FAdj (F,{a})) such that
B: ( c1 in F & c2 in F & b = c1 + ((@ ((FAdj (F,{a})),a)) * c2) ) by AA, XYZb;
b ^2 = ((c1 ^2) + ((2 '*' c1) * ((@ ((FAdj (F,{a})),a)) * c2))) + (((@ ((FAdj (F,{a})),a)) * c2) ^2) by B, REALALG2:7
.= ((c1 ^2) + ((2 '*' c1) * ((@ ((FAdj (F,{a})),a)) * c2))) + (((@ ((FAdj (F,{a})),a)) ^2) * (c2 ^2)) by FIELD_9:2
.= ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) + ((2 '*' c1) * ((@ ((FAdj (F,{a})),a)) * c2)) by RLVECT_1:def 3
.= ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) + (2 '*' (c1 * (c2 * (@ ((FAdj (F,{a})),a))))) by REALALG2:5
.= ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) + (2 '*' ((c1 * c2) * (@ ((FAdj (F,{a})),a)))) by GROUP_1:def 3
.= ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) + ((2 '*' (@ ((FAdj (F,{a})),a))) * (c1 * c2)) by REALALG2:5 ;
then E: d * (b ^2) = (d * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2)))) + (d * ((2 '*' (@ ((FAdj (F,{a})),a))) * (c1 * c2))) by VECTSP_1:def 2
.= (d * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2)))) + ((d * (c1 * c2)) * (2 '*' (@ ((FAdj (F,{a})),a)))) by GROUP_1:def 3
.= (d * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2)))) + ((2 '*' (@ ((FAdj (F,{a})),a))) * ((d * c1) * c2)) by GROUP_1:def 3 ;
set g1 = <*(d * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))))*>;
set g2 = <*((d * c1) * c2)*>;
C: Sum f = (d * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2)))) + ((2 '*' (@ ((FAdj (F,{a})),a))) * ((d * c1) * c2)) by H, A, E, RLVECT_1:44
.= (Sum <*(d * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))))*>) + ((2 '*' (@ ((FAdj (F,{a})),a))) * ((d * c1) * c2)) by RLVECT_1:44
.= (Sum <*(d * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))))*>) + ((2 '*' (@ ((FAdj (F,{a})),a))) * (Sum <*((d * c1) * c2)*>)) by RLVECT_1:44
.= (Sum <*(d * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))))*>) + (2 '*' ((@ ((FAdj (F,{a})),a)) * (Sum <*((d * c1) * c2)*>))) by REALALG2:5
.= (Sum <*(d * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))))*>) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum <*((d * c1) * c2)*>))) by REALALG2:5 ;

D: now :: thesis: for i being Element of NAT st i in dom <*(d * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))))*> holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & <*(d * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))))*> . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) )

let i be Element of NAT ; :: thesis: ( i in dom <*(d * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))))*> implies ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & <*(d * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))))*> . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) )
assume D1: i in dom <*(d * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))))*> ; :: thesis: ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & <*(d * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))))*> . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) )
dom <*(d * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))))*> = {1} by FINSEQ_1:38, FINSEQ_1:2;
then i = 1 by D1, TARSKI:def 1;
hence ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & <*(d * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))))*> . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) by A, B; :: thesis: verum

end;

now :: thesis: for i being Element of NAT st i in dom <*((d * c1) * c2)*> holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & <*((d * c1) * c2)*> . i = (b * c1) * c2 )

let i be Element of NAT ; :: thesis: ( i in dom <*((d * c1) * c2)*> implies ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & <*((d * c1) * c2)*> . i = (b * c1) * c2 ) )
assume D1: i in dom <*((d * c1) * c2)*> ; :: thesis: ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & <*((d * c1) * c2)*> . i = (b * c1) * c2 )
dom <*((d * c1) * c2)*> = {1} by FINSEQ_1:38, FINSEQ_1:2;
then i = 1 by D1, TARSKI:def 1;
hence ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & <*((d * c1) * c2)*> . i = (b * c1) * c2 ) by A, B; :: thesis: verum

end;

hence ex g1, g2 being non empty FinSequence of (FAdj (F,{a})) st
( Sum f = (Sum g1) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum g2))) & ( for i being Element of NAT st i in dom g1 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g1 . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) ) & ( for i being Element of NAT st i in dom g2 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g2 . i = (b * c1) * c2 ) ) ) by C, D; :: thesis: verum

end;

then IA: S₁[1] ;

IS: now :: thesis: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume IV: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for f being non empty P -quadratic FinSequence of (FAdj (F,{a})) st len f = k + 1 holds
ex g1, g2 being non empty FinSequence of (FAdj (F,{a})) st
( Sum f = (Sum g1) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum g2))) & ( for i being Element of NAT st i in dom g1 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g1 . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) ) & ( for i being Element of NAT st i in dom g2 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g2 . i = (b * c1) * c2 ) ) )

let f be non empty P -quadratic FinSequence of (FAdj (F,{a})); :: thesis: ( len f = k + 1 implies ex g1, g2 being non empty FinSequence of (FAdj (F,{a})) st
( Sum g1 = (Sum g2) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum b₃))) & ( for i being Element of NAT st b₄ in dom g2 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in P & c2 in F & b₇ in F & g2 . b = c1 * ((c2 ^2) + ((b₇ ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) ) & ( for i being Element of NAT st b₄ in dom i holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in P & c2 in F & b₇ in F & i . b = (c1 * c2) * b₇ ) ) ) )
assume AS: len f = k + 1 ; :: thesis: ex g1, g2 being non empty FinSequence of (FAdj (F,{a})) st
( Sum g1 = (Sum g2) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum b₃))) & ( for i being Element of NAT st b₄ in dom g2 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in P & c2 in F & b₇ in F & g2 . b = c1 * ((c2 ^2) + ((b₇ ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) ) & ( for i being Element of NAT st b₄ in dom i holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in P & c2 in F & b₇ in F & i . b = (c1 * c2) * b₇ ) ) )
consider G being FinSequence, y being object such that
A1: f = G ^ <*y*> by FINSEQ_1:46;
rng G c= rng f by A1, FINSEQ_1:29;
then reconsider G = G as FinSequence of (FAdj (F,{a})) by XBOOLE_1:1, FINSEQ_1:def 4;
A5: rng f c= the carrier of (FAdj (F,{a})) ;
A6: rng <*y*> c= rng f by A1, FINSEQ_1:30;
( rng <*y*> = {y} & y in {y} ) by FINSEQ_1:38, TARSKI:def 1;
then reconsider y = y as Element of (FAdj (F,{a})) by A5, A6;
A3: len f = (len G) + (len <*y*>) by A1, FINSEQ_1:22
.= (len G) + 1 by FINSEQ_1:39 ;

per cases ( G is empty or not G is empty ) ;

suppose G is empty ; :: thesis: ex g1, g2 being non empty FinSequence of (FAdj (F,{a})) st
( Sum g1 = (Sum g2) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum b₃))) & ( for i being Element of NAT st b₄ in dom g2 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in P & c2 in F & b₇ in F & g2 . b = c1 * ((c2 ^2) + ((b₇ ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) ) & ( for i being Element of NAT st b₄ in dom i holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in P & c2 in F & b₇ in F & i . b = (c1 * c2) * b₇ ) ) )

then f = <*y*> by A1, FINSEQ_1:34;
then len f = 1 by FINSEQ_1:40;
hence ex g1, g2 being non empty FinSequence of (FAdj (F,{a})) st
( Sum f = (Sum g1) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum g2))) & ( for i being Element of NAT st i in dom g1 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g1 . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) ) & ( for i being Element of NAT st i in dom g2 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g2 . i = (b * c1) * c2 ) ) ) by II; :: thesis: verum

end;

suppose A5: not G is empty ; :: thesis: ex g1, g2 being non empty FinSequence of (FAdj (F,{a})) st
( Sum g1 = (Sum g2) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum b₃))) & ( for i being Element of NAT st b₄ in dom g2 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in P & c2 in F & b₇ in F & g2 . b = c1 * ((c2 ^2) + ((b₇ ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) ) & ( for i being Element of NAT st b₄ in dom i holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in P & c2 in F & b₇ in F & i . b = (c1 * c2) * b₇ ) ) )

( <*y*> is FinSequence of (FAdj (F,{a})) & f = G ^ <*y*> ) by A1;
then B: ( G is P -quadratic & <*y*> is P -quadratic ) by XYZbS3a;
then consider h1, h2 being non empty FinSequence of (FAdj (F,{a})) such that
C: ( Sum G = (Sum h1) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum h2))) & ( for i being Element of NAT st i in dom h1 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & h1 . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) ) & ( for i being Element of NAT st i in dom h2 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & h2 . i = (b * c1) * c2 ) ) ) by A5, AS, A3, IV;
len <*y*> = 1 by FINSEQ_1:40;
then consider y1, y2 being non empty FinSequence of (FAdj (F,{a})) such that
D: ( Sum <*y*> = (Sum y1) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum y2))) & ( for i being Element of NAT st i in dom y1 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & y1 . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) ) & ( for i being Element of NAT st i in dom y2 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & y2 . i = (b * c1) * c2 ) ) ) by B, II;
set g1 = h1 ^ y1;
set g2 = h2 ^ y2;
E: (Sum (h1 ^ y1)) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum (h2 ^ y2)))) = ((Sum h1) + (Sum y1)) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum (h2 ^ y2)))) by RLVECT_1:41
.= ((Sum h1) + (Sum y1)) + ((@ ((FAdj (F,{a})),a)) * (2 '*' ((Sum h2) + (Sum y2)))) by RLVECT_1:41
.= ((Sum h1) + (Sum y1)) + (2 '*' (((Sum h2) + (Sum y2)) * (@ ((FAdj (F,{a})),a)))) by REALALG2:5
.= ((Sum h1) + (Sum y1)) + (2 '*' (((Sum h2) * (@ ((FAdj (F,{a})),a))) + ((Sum y2) * (@ ((FAdj (F,{a})),a))))) by VECTSP_1:def 3
.= ((Sum h1) + (Sum y1)) + ((((Sum h2) * (@ ((FAdj (F,{a})),a))) + ((Sum y2) * (@ ((FAdj (F,{a})),a)))) + (((Sum h2) * (@ ((FAdj (F,{a})),a))) + ((Sum y2) * (@ ((FAdj (F,{a})),a))))) by RING_5:2
.= ((Sum h1) + (Sum y1)) + (((Sum h2) * (@ ((FAdj (F,{a})),a))) + (((Sum y2) * (@ ((FAdj (F,{a})),a))) + (((Sum h2) * (@ ((FAdj (F,{a})),a))) + ((Sum y2) * (@ ((FAdj (F,{a})),a)))))) by RLVECT_1:def 3
.= ((Sum h1) + (Sum y1)) + (((Sum h2) * (@ ((FAdj (F,{a})),a))) + ((((Sum y2) * (@ ((FAdj (F,{a})),a))) + ((Sum y2) * (@ ((FAdj (F,{a})),a)))) + ((Sum h2) * (@ ((FAdj (F,{a})),a))))) by RLVECT_1:def 3
.= ((Sum h1) + (Sum y1)) + ((((Sum h2) * (@ ((FAdj (F,{a})),a))) + ((Sum h2) * (@ ((FAdj (F,{a})),a)))) + (((Sum y2) * (@ ((FAdj (F,{a})),a))) + ((Sum y2) * (@ ((FAdj (F,{a})),a))))) by RLVECT_1:def 3
.= ((Sum h1) + (Sum y1)) + ((2 '*' ((Sum h2) * (@ ((FAdj (F,{a})),a)))) + (((Sum y2) * (@ ((FAdj (F,{a})),a))) + ((Sum y2) * (@ ((FAdj (F,{a})),a))))) by RING_5:2
.= ((Sum h1) + (Sum y1)) + (((2 '*' (Sum h2)) * (@ ((FAdj (F,{a})),a))) + (((Sum y2) * (@ ((FAdj (F,{a})),a))) + ((Sum y2) * (@ ((FAdj (F,{a})),a))))) by REALALG2:5
.= ((Sum h1) + (Sum y1)) + (((2 '*' (Sum h2)) * (@ ((FAdj (F,{a})),a))) + (2 '*' ((Sum y2) * (@ ((FAdj (F,{a})),a))))) by RING_5:2
.= ((Sum h1) + (Sum y1)) + (((2 '*' (Sum h2)) * (@ ((FAdj (F,{a})),a))) + ((2 '*' (Sum y2)) * (@ ((FAdj (F,{a})),a)))) by REALALG2:5
.= (((Sum h1) + (Sum y1)) + ((2 '*' (Sum h2)) * (@ ((FAdj (F,{a})),a)))) + ((2 '*' (Sum y2)) * (@ ((FAdj (F,{a})),a))) by RLVECT_1:def 3
.= ((Sum y1) + ((Sum h1) + ((2 '*' (Sum h2)) * (@ ((FAdj (F,{a})),a))))) + ((2 '*' (Sum y2)) * (@ ((FAdj (F,{a})),a))) by RLVECT_1:def 3
.= ((Sum h1) + ((2 '*' (Sum h2)) * (@ ((FAdj (F,{a})),a)))) + ((Sum y1) + ((2 '*' (Sum y2)) * (@ ((FAdj (F,{a})),a)))) by RLVECT_1:def 3
.= Sum f by C, D, A1, RLVECT_1:41 ;

F: now :: thesis: for i being Element of NAT st i in dom (h1 ^ y1) holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & (h1 ^ y1) . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) )

let i be Element of NAT ; :: thesis: ( i in dom (h1 ^ y1) implies ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in P & c2 in F & b₄ in F & (h1 ^ y1) . b = c1 * ((c2 ^2) + ((b₄ ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) )
assume i in dom (h1 ^ y1) ; :: thesis: ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in P & c2 in F & b₄ in F & (h1 ^ y1) . b = c1 * ((c2 ^2) + ((b₄ ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) )

per cases then ( i in dom h1 or ex n being Nat st
( n in dom y1 & i = (len h1) + n ) ) by FINSEQ_1:25;

suppose F1: i in dom h1 ; :: thesis: ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in P & c2 in F & b₄ in F & (h1 ^ y1) . b = c1 * ((c2 ^2) + ((b₄ ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) )

then (h1 ^ y1) . i = h1 . i by FINSEQ_1:def 7;
hence ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & (h1 ^ y1) . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) by F1, C; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom y1 & i = (len h1) + n ) ; :: thesis: ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in P & c2 in F & b₄ in F & (h1 ^ y1) . b = c1 * ((c2 ^2) + ((b₄ ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) )

then consider n being Nat such that
F1: ( n in dom y1 & i = (len h1) + n ) ;
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & y1 . n = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) by F1, D;
hence ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & (h1 ^ y1) . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) by F1, FINSEQ_1:def 7; :: thesis: verum

end;

end;

end;

now :: thesis: for i being Element of NAT st i in dom (h2 ^ y2) holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & (h2 ^ y2) . i = (b * c1) * c2 )

let i be Element of NAT ; :: thesis: ( i in dom (h2 ^ y2) implies ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in P & c2 in F & b₄ in F & (h2 ^ y2) . b = (c1 * c2) * b₄ ) )
assume i in dom (h2 ^ y2) ; :: thesis: ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in P & c2 in F & b₄ in F & (h2 ^ y2) . b = (c1 * c2) * b₄ )

per cases then ( i in dom h2 or ex n being Nat st
( n in dom y2 & i = (len h2) + n ) ) by FINSEQ_1:25;

suppose F1: i in dom h2 ; :: thesis: ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in P & c2 in F & b₄ in F & (h2 ^ y2) . b = (c1 * c2) * b₄ )

then (h2 ^ y2) . i = h2 . i by FINSEQ_1:def 7;
hence ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & (h2 ^ y2) . i = (b * c1) * c2 ) by F1, C; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom y2 & i = (len h2) + n ) ; :: thesis: ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( c1 in P & c2 in F & b₄ in F & (h2 ^ y2) . b = (c1 * c2) * b₄ )

then consider n being Nat such that
F1: ( n in dom y2 & i = (len h2) + n ) ;
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & y2 . n = (b * c1) * c2 ) by F1, D;
hence ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & (h2 ^ y2) . i = (b * c1) * c2 ) by F1, FINSEQ_1:def 7; :: thesis: verum

end;

end;

end;

hence ex g1, g2 being non empty FinSequence of (FAdj (F,{a})) st
( Sum f = (Sum g1) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum g2))) & ( for i being Element of NAT st i in dom g1 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g1 . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) ) & ( for i being Element of NAT st i in dom g2 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g2 . i = (b * c1) * c2 ) ) ) by E, F; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

I: for k being non zero Nat holds S₁[k] from NAT_1:sch 10(IA, IS);
consider n being Nat such that
H: n = len f ;
thus ex g1, g2 being non empty FinSequence of (FAdj (F,{a})) st
( Sum f = (Sum g1) + ((@ ((FAdj (F,{a})),a)) * (2 '*' (Sum g2))) & ( for i being Element of NAT st i in dom g1 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g1 . i = b * ((c1 ^2) + ((c2 ^2) * ((@ ((FAdj (F,{a})),a)) ^2))) ) ) & ( for i being Element of NAT st i in dom g2 holds
ex b being non zero Element of (FAdj (F,{a})) ex c1, c2 being Element of (FAdj (F,{a})) st
( b in P & c1 in F & c2 in F & g2 . i = (b * c1) * c2 ) ) ) by H, I; :: thesis: verum