let R be commutative Ring; :: thesis:
let a, b be Element of R; :: thesis:
assume AS: ( a is square & b is sum_of_squares ) ; :: thesis:
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;

let i be Nat; :: thesis:
assume C: i in dom (a * f) ; :: thesis:
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:

end;