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

end;

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