let R be commutative Ring; :: thesis: for a, b being Element of R st a is square & b is sum_of_squares holds
a * b is sum_of_squares
let a, b be Element of R; :: thesis: ( a is square & b is sum_of_squares implies a * b is sum_of_squares )
assume AS: ( a is square & b is sum_of_squares ) ; :: thesis: a * b is sum_of_squares
then consider f being FinSequence of R such that
A: ( Sum f = b & ( for i being Nat st i in dom f holds
ex x being Element of R st f . i = x ^2 ) ) ;
set g = a * f;
B: Sum (a * f) = a * b by A, BINOM:4;

now :: thesis: for i being Nat st i in dom (a * f) holds
ex z being Element of R st (a * f) . i = z ^2

let i be Nat; :: thesis: ( i in dom (a * f) implies ex z being Element of R st (a * f) . i = z ^2 )
assume C: i in dom (a * f) ; :: thesis: ex z being Element of R st (a * f) . i = z ^2
then D: i in dom f by POLYNOM1:def 1;
E: (a * f) . i = (a * f) /. i by C, PARTFUN1:def 6
.= a * (f /. i) by D, POLYNOM1:def 1 ;
consider x being Element of R such that
F: f . i = x ^2 by D, A;
consider y being Element of R such that
G: a = y ^2 by AS;
(a * f) . i = (y ^2) * (x ^2) by E, G, D, F, PARTFUN1:def 6
.= x * (x * (y * y)) by GROUP_1:def 3
.= x * ((x * y) * y) by GROUP_1:def 3
.= (x * y) ^2 by GROUP_1:def 3 ;
hence ex z being Element of R st (a * f) . i = z ^2 ; :: thesis: verum

end;

hence a * b is sum_of_squares by B; :: thesis: verum