let R be non empty doubleLoopStr ; :: thesis: for x being Scalar of R st x is being_a_square holds
<*x*> is being_a_Product_of_squares
let x be Scalar of R; :: thesis: ( x is being_a_square implies <*x*> is being_a_Product_of_squares )
A1: for n being Nat st n <> 0 & n < len <*x*> holds
ex y being Scalar of R st
( y is being_a_square & <*x*> /. (n + 1) = (<*x*> /. n) * y )
proof
let n be Nat; :: thesis: ( n <> 0 & n < len <*x*> implies ex y being Scalar of R st
( y is being_a_square & <*x*> /. (n + 1) = (<*x*> /. n) * y ) )
assume that
A2: n <> 0 and
A3: n < len <*x*> ; :: thesis: ex y being Scalar of R st
( y is being_a_square & <*x*> /. (n + 1) = (<*x*> /. n) * y )
n < 1 by A3, Lm2;
hence ex y being Scalar of R st
( y is being_a_square & <*x*> /. (n + 1) = (<*x*> /. n) * y ) by A2, NAT_1:25; :: thesis: verum
end;
assume x is being_a_square ; :: thesis: <*x*> is being_a_Product_of_squares
then A4: <*x*> /. 1 is being_a_square by Lm2;
len <*x*> = 1 by Lm2;
hence <*x*> is being_a_Product_of_squares by A4, A1; :: thesis: verum