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 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 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 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: ( Sum f in QS (E,P) & Sum g in QS (E,P) implies (Sum f) * (Sum g) in QS (E,P) )
assume AS: ( Sum f in QS (E,P) & Sum g in QS (E,P) ) ; :: thesis: (Sum f) * (Sum g) in QS (E,P)
defpred S₁[ Nat] means 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);

now :: thesis: for f, g being P -quadratic FinSequence of E st len f = 0 & 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 = 0 & Sum g in QS (E,P) implies (Sum f) * (Sum g) in QS (E,P) )
assume ( len f = 0 & Sum g in QS (E,P) ) ; :: thesis: (Sum f) * (Sum g) in QS (E,P)
then f = <*> the carrier of E ;
then Sum f = 0. E by RLVECT_1:43;
hence (Sum f) * (Sum g) in QS (E,P) ; :: 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 f, g being P -quadratic FinSequence of E st len f = k + 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 = k + 1 & Sum f in QS (E,P) & Sum g in QS (E,P) implies (Sum b₁) * (Sum b₂) in QS (E,P) )
assume B0: ( len f = k + 1 & Sum f in QS (E,P) & Sum g in QS (E,P) ) ; :: thesis: (Sum b₁) * (Sum b₂) in QS (E,P)
then reconsider f1 = f as non empty P -quadratic FinSequence of E ;
consider h being FinSequence, x being object such that
B1: f1 = h ^ <*x*> by FINSEQ_1:46;

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

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

then f = <*x*> by B1, FINSEQ_1:34;
hence (Sum f) * (Sum g) in QS (E,P) by B0, S1, FINSEQ_1:40; :: thesis: verum

end;

suppose not h is empty ; :: thesis: (Sum b₁) * (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;
f1 = h ^ r by B1;
then reconsider h = h, r = r as P -quadratic FinSequence of E by XYZbS3a;
len r = 1 by FINSEQ_1:39;
then B2: len f = (len h) + 1 by B1, FINSEQ_1:22;
Sum h in QS (E,P) ;
then (Sum h) * (Sum g) in QS (E,P) by B0, B2, IV;
then consider hg being P -quadratic FinSequence of E such that
B3: Sum hg = (Sum h) * (Sum g) ;
( Sum r in QS (E,P) & len r = 1 ) by FINSEQ_1:39;
then (Sum r) * (Sum g) in QS (E,P) by B0, S1;
then consider rg being P -quadratic FinSequence of E such that
B4: Sum rg = (Sum r) * (Sum g) ;
(Sum f) * (Sum g) = ((Sum h) + (Sum r)) * (Sum g) by B1, RLVECT_1:41
.= (Sum hg) + (Sum rg) by B3, B4, VECTSP_1:def 2
.= Sum (hg ^ rg) 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 f = n ;
thus (Sum f) * (Sum g) in QS (E,P) by AS, I, H; :: thesis: verum