let b, n be Element of NAT ; :: thesis: GenFib (0,b,n) = b * (Fib n)

defpred S_{1}[ Nat] means GenFib (0,b,$1) = b * (Fib $1);

A1: S_{1}[1]
by Th32, PRE_FF:1;

A2: for k being Nat st S_{1}[k] & S_{1}[k + 1] holds

S_{1}[k + 2]
_{1}[ 0 ]
by Th32, PRE_FF:1;

for k being Nat holds S_{1}[k]
from FIB_NUM:sch 1(A5, A1, A2);

hence GenFib (0,b,n) = b * (Fib n) ; :: thesis: verum

defpred S

A1: S

A2: for k being Nat st S

S

proof

A5:
S
let k be Nat; :: thesis: ( S_{1}[k] & S_{1}[k + 1] implies S_{1}[k + 2] )

assume that

A3: S_{1}[k]
and

A4: S_{1}[k + 1]
; :: thesis: S_{1}[k + 2]

GenFib (0,b,(k + 2)) = (b * (Fib k)) + (GenFib (0,b,(k + 1))) by A3, Th34

.= b * ((Fib k) + (Fib (k + 1))) by A4

.= b * (Fib (k + 2)) by FIB_NUM2:24 ;

hence S_{1}[k + 2]
; :: thesis: verum

end;assume that

A3: S

A4: S

GenFib (0,b,(k + 2)) = (b * (Fib k)) + (GenFib (0,b,(k + 1))) by A3, Th34

.= b * ((Fib k) + (Fib (k + 1))) by A4

.= b * (Fib (k + 2)) by FIB_NUM2:24 ;

hence S

for k being Nat holds S

hence GenFib (0,b,n) = b * (Fib n) ; :: thesis: verum