let f be Complex_Sequence; :: thesis: for n, m being Nat st f . n = 0 holds
(Partial_Product f) . (n + m) = 0
let n, m be Nat; :: thesis: ( f . n = 0 implies (Partial_Product f) . (n + m) = 0 )
assume A1: f . n = 0 ; :: thesis: (Partial_Product f) . (n + m) = 0
defpred S₁[ Nat] means (Partial_Product f) . (n + $1) = 0 ;
A2: S₁[ 0 ] by A1, PPN;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B1: S₁[k] ; :: thesis: S₁[k + 1]
(Partial_Product f) . ((n + k) + 1) = ((Partial_Product f) . (n + k)) * (f . ((n + k) + 1)) by PP;
hence S₁[k + 1] by B1; :: thesis: verum

end;

for x being Nat holds S₁[x] from NAT_1:sch 2(A2, A3);
hence (Partial_Product f) . (n + m) = 0 ; :: thesis: verum