let b, n be Element of NAT ; GenFib (0,b,n) = b * (Fib n)
defpred S1[ Nat] means GenFib (0,b,$1) = b * (Fib $1);
A1:
S1[1]
by Th32, PRE_FF:1;
A2:
for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
A5:
S1[ 0 ]
by Th32, PRE_FF:1;
for k being Nat holds S1[k]
from FIB_NUM:sch 1(A5, A1, A2);
hence
GenFib (0,b,n) = b * (Fib n)
; verum