let R be non empty doubleLoopStr ; :: thesis: for x being Scalar of R st x is being_a_square holds
<*x*> is being_a_generation_from_squares
let x be Scalar of R; :: thesis: ( x is being_a_square implies <*x*> is being_a_generation_from_squares )
assume x is being_a_square ; :: thesis: <*x*> is being_a_generation_from_squares
then A1: x is being_an_amalgam_of_squares by Lm17;
A2: len <*x*> = 1 by Lm2;
A3: <*x*> /. 1 is being_an_amalgam_of_squares by A1, Lm2;
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 ( n <> 0 & 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 ) )
then ( n <> 0 & n <= 1 ) 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 A3, NAT_1:26; :: thesis: verum

end;

hence <*x*> is being_a_generation_from_squares by A2, Def14; :: thesis: verum