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: S₁[ 0 ] by Th32, PRE_FF:1;
A2: 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 ;
Fib 2 = Fib (0 + 2)
.= 0 + 1 by FIB_NUM2:26, PRE_FF:1 ;
then A3: S₁[1] by A2, PRE_FF:1;
A4: 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
A5: S₁[k] and
A6: 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 A5, Th34
.= (a * ((Fib k) + (Fib (k + 1)))) + (b * ((Fib (k + 1)) + (Fib ((k + 1) + 1)))) by A6
.= (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;

for k being Nat holds S₁[k] from FIB_NUM:sch 1(A1, A3, A4);
hence GenFib a,b,(n + 1) = (a * (Fib n)) + (b * (Fib (n + 1))) ; :: thesis: verum