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