let R be non empty doubleLoopStr ; :: thesis: for x being Scalar of R st x is being_an_amalgam_of_squares holds
<*x*> is being_a_generation_from_squares
let x be Scalar of R; :: thesis: ( x is being_an_amalgam_of_squares implies <*x*> is being_a_generation_from_squares )
set g = <*x*>;
assume A1: x is being_an_amalgam_of_squares ; :: thesis: <*x*> is being_a_generation_from_squares
A2: 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 by A4, Lm2;
then n < 1 + 1 by NAT_1:13;
then n = 1 by A3, NAT_1:23;
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 A1, Lm2; :: thesis: verum

end;

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