let F be ordered Field; :: thesis: for P being Ordering of F
for E being FieldExtension of F
for f, g being b₁ -quadratic FinSequence of E st len f = 1 & Sum f in QS (E,P) & Sum g in QS (E,P) holds
(Sum f) * (Sum g) in QS (E,P)
let P be Ordering of F; :: thesis: for E being FieldExtension of F
for f, g being P -quadratic FinSequence of E st len f = 1 & Sum f in QS (E,P) & Sum g in QS (E,P) holds
(Sum f) * (Sum g) in QS (E,P)
let E be FieldExtension of F; :: thesis: for f, g being P -quadratic FinSequence of E st len f = 1 & Sum f in QS (E,P) & Sum g in QS (E,P) holds
(Sum f) * (Sum g) in QS (E,P)
let f, g be P -quadratic FinSequence of E; :: thesis: ( len f = 1 & Sum f in QS (E,P) & Sum g in QS (E,P) implies (Sum f) * (Sum g) in QS (E,P) )
assume AS: ( len f = 1 & Sum f in QS (E,P) & Sum g in QS (E,P) ) ; :: thesis: (Sum f) * (Sum g) in QS (E,P)
H0: f = <*(f . 1)*> by AS, FINSEQ_1:40;
then dom f = {1} by FINSEQ_1:2, FINSEQ_1:38;
then H1: 1 in dom f by TARSKI:def 1;
rng f c= the carrier of E ;
then reconsider u = f . 1 as Element of E by H1, FUNCT_1:3;
consider ua being non zero Element of E, ub being Element of E such that
H2: ( ua in P & u = ua * (ub ^2) ) by H1, dq;
I: F is Subfield of E by FIELD_4:7;
defpred S₁[ Nat] means for g being P -quadratic FinSequence of E st len g = $1 & Sum g in QS (E,P) holds
(Sum f) * (Sum g) in QS (E,P);

now :: thesis: for g being P -quadratic FinSequence of E st len g = 0 & Sum g in QS (E,P) holds
(Sum f) * (Sum g) in QS (E,P)

let g be P -quadratic FinSequence of E; :: thesis: ( len g = 0 & Sum g in QS (E,P) implies (Sum f) * (Sum g) in QS (E,P) )
assume ( len g = 0 & Sum g in QS (E,P) ) ; :: thesis: (Sum f) * (Sum g) in QS (E,P)
then g = <*> the carrier of E ;
then B: Sum g = 0. E by RLVECT_1:43;
reconsider h = <*(0. E)*> as non empty FinSequence of E ;
thus (Sum f) * (Sum g) in QS (E,P) by B; :: thesis: verum

end;

then IA: S₁[ 0 ] ;

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

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

now :: thesis: for g being P -quadratic FinSequence of E st len g = k + 1 & Sum g in QS (E,P) holds
(Sum f) * (Sum g) in QS (E,P)

let g be P -quadratic FinSequence of E; :: thesis: ( len g = k + 1 & Sum g in QS (E,P) implies (Sum f) * (Sum b₁) in QS (E,P) )
assume B0: ( len g = k + 1 & Sum g in QS (E,P) ) ; :: thesis: (Sum f) * (Sum b₁) in QS (E,P)
then g <> {} ;
then consider h being FinSequence, x being object such that
B1: g = h ^ <*x*> by FINSEQ_1:46;

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

suppose h is empty ; :: thesis: (Sum f) * (Sum b₁) in QS (E,P)

then B3: g = <*x*> by B1, FINSEQ_1:34;
then dom g = {1} by FINSEQ_1:2, FINSEQ_1:38;
then B2: 1 in dom g by TARSKI:def 1;
B5: g . 1 = x by B3;
rng g c= the carrier of E ;
then reconsider x = x as Element of E by B5, B2, FUNCT_1:3;
consider xa being non zero Element of E, xb being Element of E such that
B4: ( xa in P & x = xa * (xb ^2) ) by B2, dq, B5;
reconsider r = <*(u * x)*> as non empty FinSequence of E ;
B5: ua * xa in P

proof

reconsider z1 = ua, z2 = xa as Element of F by H2, B4;
C2: [z1,z2] in [: the carrier of F, the carrier of F:] ;
z1 * z2 = ( the multF of E || the carrier of F) . (z1,z2) by I, EC_PF_1:def 1
.= ua * xa by C2, FUNCT_1:49 ;
hence ua * xa in P by H2, B4, REALALG1:def 5; :: thesis: verum

end;

B6: Sum r = u * x by RLVECT_1:44
.= (Sum f) * x by H0, RLVECT_1:44
.= (Sum f) * (Sum g) by B3, RLVECT_1:44 ;
B9: dom r = {1} by FINSEQ_1:2, FINSEQ_1:38;
B8: r . 1 = (ua * (ub ^2)) * (xa * (xb ^2)) by B4, H2
.= ua * ((ub ^2) * (xa * (xb ^2))) by GROUP_1:def 3
.= ua * (((ub ^2) * (xb ^2)) * xa) by GROUP_1:def 3
.= (ua * xa) * ((ub ^2) * (xb ^2)) by GROUP_1:def 3
.= (ua * xa) * ((ub * xb) ^2) by FIELD_9:2 ;
r is P -quadratic

proof

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

let i be Element of NAT ; :: thesis: ( i in dom r implies ex c being non zero Element of E ex b being Element of E st
( c in P & r . i = c * (b ^2) ) )
assume AS: i in dom r ; :: thesis: ex c being non zero Element of E ex b being Element of E st
( c in P & r . i = c * (b ^2) )
thus ex c being non zero Element of E ex b being Element of E st
( c in P & r . i = c * (b ^2) ) :: thesis: verum

proof

r . i = (ua * xa) * ((ub * xb) ^2) by AS, B8, B9, TARSKI:def 1;
hence ex c being non zero Element of E ex b being Element of E st
( c in P & r . i = c * (b ^2) ) by B5; :: thesis: verum

end;

end;

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

end;

hence (Sum f) * (Sum g) in QS (E,P) by B6; :: thesis: verum

end;

suppose not h is empty ; :: thesis: (Sum f) * (Sum b₁) in QS (E,P)

then reconsider h = h as non empty FinSequence of E by B1, FINSEQ_1:36;
reconsider r = <*x*> as non empty FinSequence of E by B1, FINSEQ_1:36;
len r = 1 by FINSEQ_1:39;
then B2: len g = (len h) + 1 by B1, FINSEQ_1:22;
reconsider g1 = g as non empty P -quadratic FinSequence of E by B0;
g1 = h ^ r by B1;
then reconsider h = h, r = r as non empty P -quadratic FinSequence of E by XYZbS3a;
Sum h in QS (E,P) ;
then (Sum f) * (Sum h) in QS (E,P) by B0, B2, IV;
then consider fh being P -quadratic FinSequence of E such that
B3: Sum fh = (Sum f) * (Sum h) ;
(Sum f) * (Sum r) in QS (E,P)

proof

dom r = {1} by FINSEQ_1:2, FINSEQ_1:38;
then B2: 1 in dom r by TARSKI:def 1;
B5: r . 1 = x ;
rng r c= the carrier of E ;
then reconsider x = x as Element of E by B5, B2, FUNCT_1:3;
len r = 1 by FINSEQ_1:39;
then E0: len g = (len h) + 1 by B1, FINSEQ_1:22;
E2: dom g = Seg (k + 1) by B0, FINSEQ_1:def 3;
E5: x = g . (k + 1) by E0, B0, B1, FINSEQ_1:42;
consider xa being non zero Element of E, xb being Element of E such that
C1: ( xa in P & x = xa * (xb ^2) ) by E5, dq, E2, FINSEQ_1:4;
reconsider l = <*(u * x)*> as non empty FinSequence of E ;
C2: ua * xa in P

proof

reconsider z1 = ua, z2 = xa as Element of F by H2, C1;
D2: [z1,z2] in [: the carrier of F, the carrier of F:] ;
z1 * z2 = ( the multF of E || the carrier of F) . (z1,z2) by I, EC_PF_1:def 1
.= ua * xa by D2, FUNCT_1:49 ;
hence ua * xa in P by H2, C1, REALALG1:def 5; :: thesis: verum

end;

B6: Sum l = u * x by RLVECT_1:44
.= (Sum f) * x by H0, RLVECT_1:44
.= (Sum f) * (Sum r) by RLVECT_1:44 ;
B9: dom l = {1} by FINSEQ_1:2, FINSEQ_1:38;
B8: l . 1 = (ua * (ub ^2)) * (xa * (xb ^2)) by C1, H2
.= ua * ((ub ^2) * (xa * (xb ^2))) by GROUP_1:def 3
.= ua * (((ub ^2) * (xb ^2)) * xa) by GROUP_1:def 3
.= (ua * xa) * ((ub ^2) * (xb ^2)) by GROUP_1:def 3
.= (ua * xa) * ((ub * xb) ^2) by FIELD_9:2 ;
l is P -quadratic

proof

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

let i be Element of NAT ; :: thesis: ( i in dom l implies ex c being non zero Element of E ex b being Element of E st
( c in P & l . i = c * (b ^2) ) )
assume AS: i in dom l ; :: thesis: ex c being non zero Element of E ex b being Element of E st
( c in P & l . i = c * (b ^2) )
thus ex c being non zero Element of E ex b being Element of E st
( c in P & l . i = c * (b ^2) ) :: thesis: verum

proof

l . i = (ua * xa) * ((ub * xb) ^2) by AS, B8, B9, TARSKI:def 1;
hence ex c being non zero Element of E ex b being Element of E st
( c in P & l . i = c * (b ^2) ) by C2; :: thesis: verum

end;

end;

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

end;

hence (Sum f) * (Sum r) in QS (E,P) by B6; :: thesis: verum

end;

then consider fr being P -quadratic FinSequence of E such that
B4: Sum fr = (Sum f) * (Sum r) ;
(Sum f) * (Sum g) = (Sum f) * ((Sum h) + (Sum r)) by B1, RLVECT_1:41
.= (Sum fh) + (Sum fr) by B3, B4, VECTSP_1:def 3
.= Sum (fh ^ fr) by RLVECT_1:41 ;
hence (Sum f) * (Sum g) in QS (E,P) ; :: thesis: verum

end;

end;

end;

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

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
consider n being Nat such that
H: len g = n ;
thus (Sum f) * (Sum g) in QS (E,P) by AS, I, H; :: thesis: verum