let f be Complex_Sequence; :: thesis: for n being Nat st f . n = 0 holds
(Partial_Product f) . n = 0
let n be Nat; :: thesis: ( f . n = 0 implies (Partial_Product f) . n = 0 )
assume A1: f . n = 0 ; :: thesis: (Partial_Product f) . n = 0

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: (Partial_Product f) . n = 0

hence (Partial_Product f) . n = 0 by A1, PP; :: thesis: verum

end;

suppose n > 0 ; :: thesis: (Partial_Product f) . n = 0

then reconsider m = n - 1 as Nat ;
(Partial_Product f) . (m + 1) = ((Partial_Product f) . m) * (f . (m + 1)) by PP;
hence (Partial_Product f) . n = 0 by A1; :: thesis: verum

end;

end;