let i be Nat; :: thesis: for R being non empty doubleLoopStr
for f being FinSequence of R st f is being_a_Sum_of_products_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_Sum_of_products_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_Sum_of_products_of_squares & 0 <> i & i <= len f implies f /. i is generated_from_squares )
assume that
A1: f is being_a_Sum_of_products_of_squares and
A2: 0 <> i and
A3: 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 );
A4: S₁[ 0 ] ;
A5: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

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

A9: now

assume i = 0 ; :: thesis: f /. (i + 1) is generated_from_squares
then f /. (i + 1) is being_a_product_of_squares by A1, Def8;
hence f /. (i + 1) is generated_from_squares by Lm49; :: thesis: verum

end;

now

assume A10: i <> 0 ; :: thesis: f /. (i + 1) is generated_from_squares
then ex y being Scalar of R st
( y is being_a_product_of_squares & f /. (i + 1) = (f /. i) + y ) by A1, A8, Def8;
hence f /. (i + 1) is generated_from_squares by A6, A7, A10, Lm52, NAT_1:13; :: thesis: verum

end;

hence f /. (i + 1) is generated_from_squares by A9; :: thesis: verum

end;

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