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_generation_from_squares
let x be Scalar of R; :: thesis: ( x is being_a_product_of_squares implies <*x*> is being_a_generation_from_squares )
set g = <*x*>;
A1: len <*x*> = 1 by Lm2;
assume A2: x is being_a_product_of_squares ; :: thesis: <*x*> is being_a_generation_from_squares
for n being Nat st n <> 0 & n <= len <*x*> & not <*x*> /. n is being_an_amalgam_of_squares holds
ex i, j being Nat st
( ( <*x*> /. n = (<*x*> /. i) * (<*x*> /. j) or <*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_an_amalgam_of_squares implies ex i, j being Nat st
( ( <*x*> /. n = (<*x*> /. i) * (<*x*> /. j) or <*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_an_amalgam_of_squares or ex i, j being Nat st
( ( <*x*> /. n = (<*x*> /. i) * (<*x*> /. j) or <*x*> /. n = (<*x*> /. i) + (<*x*> /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) )
n < 1 + 1 by A1, A4, NAT_1:13;
then n = 1 by A3, NAT_1:23;
then <*x*> /. n = x by Lm2;
hence ( <*x*> /. n is being_an_amalgam_of_squares or ex i, j being Nat st
( ( <*x*> /. n = (<*x*> /. i) * (<*x*> /. j) or <*x*> /. n = (<*x*> /. i) + (<*x*> /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) ) by A2, Lm19; :: thesis: verum

end;

hence <*x*> is being_a_generation_from_squares by A1; :: thesis: verum