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

proof

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

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

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

end;

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

end;

A7: S₁[ 0 ] ;
thus for i being Nat holds S₁[i] from NAT_1:sch 2(A7, A2); :: thesis: verum