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:24 ;
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