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 & i <= len f ) ; :: thesis: f /. i is generated_from_squares
defpred S1[ Nat] means ( 0 <> $1 & $1 <= len f implies f /. $1 is generated_from_squares );
A3: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A4: ( 0 <> i & i <= len f implies f /. i is generated_from_squares ) ; :: thesis: S1[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_product_of_squares & f /. (i + 1) = (f /. i) + y ) by A1, A6;
hence f /. (i + 1) is generated_from_squares by A4, A5, A8, Lm52, NAT_1:13; :: thesis: verum
end;
( i = 0 implies f /. (i + 1) is generated_from_squares ) by A1, Lm49;
hence f /. (i + 1) is generated_from_squares by A7; :: thesis: verum
end;
A9: S1[ 0 ] ;
for i being Nat holds S1[i] from NAT_1:sch 2(A9, A3);
 hence f /. i is generated_from_squares by A2; :: thesis: verum