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

proof

let n be Nat; :: thesis: ( n <> 0 & n <= len <*x*> & not <*x*> /. n is being_a_product_of_squares implies ex i, j being Nat st
( <*x*> /. n = (<*x*> /. i) * (<*x*> /. j) & i <> 0 & i < n & j <> 0 & j < n ) )
assume that
A3: n <> 0 and
A4: n <= len <*x*> ; :: thesis: ( <*x*> /. n is being_a_product_of_squares or ex i, j being Nat st
( <*x*> /. n = (<*x*> /. i) * (<*x*> /. j) & i <> 0 & i < n & j <> 0 & j < n ) )
n <= 1 by A4, Lm2;
hence ( <*x*> /. n is being_a_product_of_squares or ex i, j being Nat st
( <*x*> /. n = (<*x*> /. i) * (<*x*> /. j) & i <> 0 & i < n & j <> 0 & j < n ) ) by A1, A3, NAT_1:25; :: thesis: verum

end;

len <*x*> = 1 by Lm2;
hence <*x*> is being_an_Amalgam_of_squares by A2; :: thesis: verum