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