let a, n be Element of NAT ; :: thesis: GenFib a,0 ,(n + 1) = a * (Fib n)
defpred S₁[ Nat] means GenFib a,0 ,($1 + 1) = a * (Fib $1);
A1: 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
A2: S₁[k] and
A3: S₁[k + 1] ; :: thesis: S₁[k + 2]
GenFib a,0 ,((k + 2) + 1) = GenFib a,0 ,((k + 1) + 2)
.= (a * (Fib k)) + (GenFib a,0 ,((k + 1) + 1)) by A2, Th34
.= a * ((Fib k) + (Fib (k + 1))) by A3
.= a * (Fib (k + 2)) by FIB_NUM2:26 ;
hence S₁[k + 2] ; :: thesis: verum

end;

GenFib a,0 ,2 = GenFib a,0 ,(0 + 2)
.= (GenFib a,0 ,0 ) + (GenFib a,0 ,(0 + 1)) by Th34
.= a + (GenFib a,0 ,1) by Th32
.= a + 0 by Th32 ;
then A4: S₁[1] by PRE_FF:1;
A5: S₁[ 0 ] by Th32, PRE_FF:1;
for k being Nat holds S₁[k] from FIB_NUM:sch 1(A5, A4, A1);
hence GenFib a,0 ,(n + 1) = a * (Fib n) ; :: thesis: verum