let a, b, n be Element of NAT ; :: thesis: GenFib (a,b,(n + 1)) = (a * (Fib n)) + (b * (Fib (n + 1)))
defpred S1[ Nat] means GenFib (a,b,(\$1 + 1)) = (a * (Fib \$1)) + (b * (Fib (\$1 + 1)));
A1: Fib 2 = Fib (0 + 2)
.= 0 + 1 by ;
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: S1 by A1, PRE_FF:1;
A3: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; :: thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
A4: S1[k] and
A5: S1[k + 1] ; :: thesis: S1[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
.= (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:24
.= (a * (Fib (k + 2))) + (b * (Fib ((k + 1) + 2))) by FIB_NUM2:24
.= (a * (Fib (k + 2))) + (b * (Fib ((k + 2) + 1))) ;
hence S1[k + 2] ; :: thesis: verum
end;
A6: S1[ 0 ] by ;
for k being Nat holds S1[k] from FIB_NUM:sch 1(A6, A2, A3);
hence GenFib (a,b,(n + 1)) = (a * (Fib n)) + (b * (Fib (n + 1))) ; :: thesis: verum