let m be Element of NAT ; :: thesis: Fib (m + 1) <> 0
per cases ( m = 0 or m <> 0 ) ;
suppose m = 0 ; :: thesis: Fib (m + 1) <> 0
hence Fib (m + 1) <> 0 by PRE_FF:1; :: thesis: verum
end;
suppose m <> 0 ; :: thesis: Fib (m + 1) <> 0
hence Fib (m + 1) <> 0 by Lm3, NAT_1:3; :: thesis: verum
end;
end;