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 f /. 1 is being_a_square ;
then A2: f /. 1 is being_a_product_of_squares by Lm9;
A3: 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 ex y being Scalar of R st
( y is being_a_square & f /. (n + 1) = (f /. n) + y ) by A1;
hence ex y being Scalar of R st
( y is being_a_product_of_squares & f /. (n + 1) = (f /. n) + y ) by Lm9; :: thesis: verum

end;

len f <> 0 by A1;
hence f is being_a_Sum_of_products_of_squares by A2, A3; :: thesis: verum