theorem :: COMSEQ_3:1

for n being Nat holds
( n + 1 <> 0c & (n + 1) * <i> <> 0c ) ;