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_an_Amalgam_of_squares
let x be Scalar of R; :: thesis: ( x is being_a_product_of_squares implies <*x*> is being_an_Amalgam_of_squares )
assume A1: x is being_a_product_of_squares ; :: thesis: <*x*> is being_an_Amalgam_of_squares
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*> & 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 ( n <> 0 & 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 ) )
then ( n <> 0 & n <= 1 ) by 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 A3, NAT_1:26; :: thesis: verum

end;

hence <*x*> is being_an_Amalgam_of_squares by A2, Def10; :: thesis: verum