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

proof

let n be Nat; :: thesis: ( n <> 0 & n < len <*x*> implies ex y being Scalar of R st
( y is being_a_product_of_squares & <*x*> /. (n + 1) = (<*x*> /. n) + y ) )
assume ( n <> 0 & n < len <*x*> ) ; :: thesis: ex y being Scalar of R st
( y is being_a_product_of_squares & <*x*> /. (n + 1) = (<*x*> /. n) + y )
then ( n <> 0 & n < 1 ) by Lm2;
hence ex y being Scalar of R st
( y is being_a_product_of_squares & <*x*> /. (n + 1) = (<*x*> /. n) + y ) by NAT_1:26; :: thesis: verum

end;

hence <*x*> is being_a_Sum_of_products_of_squares by A2, A3, Def8; :: thesis: verum