let i be Nat; :: thesis: for R being non empty doubleLoopStr
for f being FinSequence of R st f is being_a_Product_of_squares & 0 <> i & i <= len f holds
f /. i is generated_from_squares
let R be non empty doubleLoopStr ; :: thesis: for f being FinSequence of R st f is being_a_Product_of_squares & 0 <> i & i <= len f holds
f /. i is generated_from_squares
let f be FinSequence of R; :: thesis: ( f is being_a_Product_of_squares & 0 <> i & i <= len f implies f /. i is generated_from_squares )
assume that
A1: f is being_a_Product_of_squares and
A2: ( 0 <> i & i <= len f ) ; :: thesis: f /. i is generated_from_squares
defpred S₁[ Nat] means ( 0 <> $1 & $1 <= len f implies f /. $1 is generated_from_squares );
A3: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: ( 0 <> i & i <= len f implies f /. i is generated_from_squares ) ; :: thesis: S₁[i + 1]
assume that
0 <> i + 1 and
A5: i + 1 <= len f ; :: thesis: f /. (i + 1) is generated_from_squares
A6: i < len f by A5, NAT_1:13;

A7: now :: thesis: ( i <> 0 implies f /. (i + 1) is generated_from_squares )

assume A8: i <> 0 ; :: thesis: f /. (i + 1) is generated_from_squares
then ex y being Scalar of R st
( y is being_a_square & f /. (i + 1) = (f /. i) * y ) by A1, A6;
hence f /. (i + 1) is generated_from_squares by A4, A5, A8, Lm47, NAT_1:13; :: thesis: verum

end;

( i = 0 implies f /. (i + 1) is generated_from_squares ) by A1, Lm31;
hence f /. (i + 1) is generated_from_squares by A7; :: thesis: verum

end;

A9: S₁[ 0 ] ;
for i being Nat holds S₁[i] from NAT_1:sch 2(A9, A3);
hence f /. i is generated_from_squares by A2; :: thesis: verum