let b, n be Element of NAT ; :: thesis: GenFib 0 ,b,n = b * (Fib n)
defpred S₁[ Nat] means GenFib 0 ,b,$1 = b * (Fib $1);
A1: S₁[1] by Th32, PRE_FF:1;
A2: for k being Nat st S₁[k] & S₁[k + 1] holds
S₁[k + 2]

proof

let k be Nat; :: thesis: ( S₁[k] & S₁[k + 1] implies S₁[k + 2] )
assume that
A3: S₁[k] and
A4: S₁[k + 1] ; :: thesis: S₁[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:26 ;
hence S₁[k + 2] ; :: thesis: verum

end;

A5: S₁[ 0 ] by Th32, PRE_FF:1;
for k being Nat holds S₁[k] from FIB_NUM:sch 1(A5, A1, A2);
hence GenFib 0 ,b,n = b * (Fib n) ; :: thesis: verum