let R be non empty doubleLoopStr ; :: thesis: for x being Scalar of R st x is being_a_product_of_squares holds
<*x*> is being_a_Sum_of_amalgams_of_squares
let x be Scalar of R; :: thesis: ( x is being_a_product_of_squares implies <*x*> is being_a_Sum_of_amalgams_of_squares )
A1: for n being Nat st n <> 0 & n < len <*x*> holds
ex y being Scalar of R st
( y is being_an_amalgam_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_an_amalgam_of_squares & <*x*> /. (n + 1) = (<*x*> /. n) + y ) )
assume that
A2: n <> 0 and
A3: n < len <*x*> ; :: thesis: ex y being Scalar of R st
( y is being_an_amalgam_of_squares & <*x*> /. (n + 1) = (<*x*> /. n) + y )
n < 1 by A3, Lm2;
hence ex y being Scalar of R st
( y is being_an_amalgam_of_squares & <*x*> /. (n + 1) = (<*x*> /. n) + y ) by A2, NAT_1:25; :: thesis: verum

end;

assume x is being_a_product_of_squares ; :: thesis: <*x*> is being_a_Sum_of_amalgams_of_squares
then x is being_an_amalgam_of_squares by Lm19;
then A4: <*x*> /. 1 is being_an_amalgam_of_squares by Lm2;
len <*x*> = 1 by Lm2;
hence <*x*> is being_a_Sum_of_amalgams_of_squares by A4, A1; :: thesis: verum