let R be commutative Ring; :: thesis: for a, b being Element of R st a is sum_of_squares & b is sum_of_squares holds
a * b is sum_of_squares
let a, b be Element of R; :: thesis: ( a is sum_of_squares & b is sum_of_squares implies a * b is sum_of_squares )
assume AS: ( a is sum_of_squares & b is sum_of_squares ) ; :: thesis: a * b is sum_of_squares
defpred S₁[ Nat] means for f being FinSequence of R st len f = $1 & ( for i being Nat st i in dom f holds
ex x being Element of R st f . i = x ^2 ) holds
a * (Sum f) is sum_of_squares ;

now :: thesis: for f being FinSequence of R st len f = 0 & ( for i being Nat st i in dom f holds
ex x being Element of R st f . i = x ^2 ) holds
a * (Sum f) is sum_of_squares

let f be FinSequence of R; :: thesis: ( len f = 0 & ( for i being Nat st i in dom f holds
ex x being Element of R st f . i = x ^2 ) implies a * (Sum f) is sum_of_squares )
assume ( len f = 0 & ( for i being Nat st i in dom f holds
ex x being Element of R st f . i = x ^2 ) ) ; :: thesis: a * (Sum f) is sum_of_squares
then f = <*> the carrier of R ;
then Sum f = 0. R by RLVECT_1:43;
hence a * (Sum f) is sum_of_squares ; :: thesis: verum

end;

then A: S₁[ 0 ] ;

B: 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 being FinSequence of R st len f = k + 1 & ( for i being Nat st i in dom f holds
ex x being Element of R st f . i = x ^2 ) holds
a * (Sum f) is sum_of_squares

let f be FinSequence of R; :: thesis: ( len f = k + 1 & ( for i being Nat st i in dom f holds
ex x being Element of R st f . i = x ^2 ) implies a * (Sum f) is sum_of_squares )
assume B0: ( len f = k + 1 & ( for i being Nat st i in dom f holds
ex x being Element of R st f . i = x ^2 ) ) ; :: thesis: a * (Sum f) is sum_of_squares
then f <> {} ;
then consider g being FinSequence, x being object such that
B1: f = g ^ <*x*> by FINSEQ_1:46;
reconsider g = g, h = <*x*> as FinSequence of R by B1, FINSEQ_1:36;
len h = 1 by FINSEQ_1:39;
then B2: len f = (len g) + 1 by B1, FINSEQ_1:22;

now :: thesis: for i being Nat st i in dom g holds
ex x being Element of R st g . i = x ^2

let i be Nat; :: thesis: ( i in dom g implies ex x being Element of R st g . i = x ^2 )
assume C1: i in dom g ; :: thesis: ex x being Element of R st g . i = x ^2
then C2: g . i = f . i by B1, FINSEQ_1:def 7;
dom g c= dom f by B1, FINSEQ_1:26;
hence ex x being Element of R st g . i = x ^2 by B0, C2, C1; :: thesis: verum

end;

then B3: a * (Sum g) is sum_of_squares by IV, B2, B0;
C2: dom f = Seg (k + 1) by B0, FINSEQ_1:def 3;
B4: 1 <= k + 1 by NAT_1:11;
B5: x = f . (k + 1) by B0, B2, B1, FINSEQ_1:42;
then reconsider x = x as Element of R by B4, C2, FINSEQ_1:1, FINSEQ_2:11;
consider z being Element of R such that
B6: x = z ^2 by B0, B4, B5, C2, FINSEQ_1:1;
x is square by B6;
then B7: x * a is sum_of_squares by S2, AS;
(a * (Sum g)) + (a * x) = a * ((Sum g) + x) by VECTSP_1:def 3
.= a * ((Sum g) + (Sum <*x*>)) by RLVECT_1:44
.= a * (Sum f) by B1, RLVECT_1:41 ;
hence a * (Sum f) is sum_of_squares by B7, B3, S1; :: thesis: verum

end;

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

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 2(A, B);
consider f being FinSequence of R such that
H: ( Sum f = b & ( for i being Nat st i in dom f holds
ex x being Element of R st f . i = x ^2 ) ) by AS;
consider k being Nat such that
K: len f = k ;
thus a * b is sum_of_squares by I, H, K; :: thesis: verum