let R be non empty doubleLoopStr ; :: thesis: for f being FinSequence of R st f is being_a_Sum_of_squares holds
f is being_a_Sum_of_products_of_squares
let f be FinSequence of R; :: thesis: ( f is being_a_Sum_of_squares implies f is being_a_Sum_of_products_of_squares )
assume A1: f is being_a_Sum_of_squares ; :: thesis: f is being_a_Sum_of_products_of_squares
then ( len f <> 0 & f /. 1 is being_a_square ) by Def4;
then A2: ( len f <> 0 & f /. 1 is being_a_product_of_squares ) by Lm9;
for n being Nat st n <> 0 & n < len f holds
ex y being Scalar of R st
( y is being_a_product_of_squares & f /. (n + 1) = (f /. n) + y )

proof

let n be Nat; :: thesis: ( n <> 0 & n < len f implies ex y being Scalar of R st
( y is being_a_product_of_squares & f /. (n + 1) = (f /. n) + y ) )
assume ( n <> 0 & n < len f ) ; :: thesis: ex y being Scalar of R st
( y is being_a_product_of_squares & f /. (n + 1) = (f /. n) + y )
then consider y being Scalar of R such that
A3: ( y is being_a_square & f /. (n + 1) = (f /. n) + y ) by A1, Def4;
thus ex y being Scalar of R st
( y is being_a_product_of_squares & f /. (n + 1) = (f /. n) + y ) by A3, Lm9; :: thesis: verum

end;

hence f is being_a_Sum_of_products_of_squares by A2, Def8; :: thesis: verum