let a, b, n be non zero Element of NAT ; :: thesis: GenFib (a,b,n) = ((GenFib (a,b,0)) * (Fib (n -' 1))) + ((GenFib (a,b,1)) * (Fib n))
thus GenFib (a,b,n) = ((GenFib (a,b,0)) * (Fib (n -' 1))) + ((GenFib (a,b,1)) * (Fib n)) :: thesis: verum

proof

defpred S₁[ Nat] means GenFib (a,b,$1) = ((GenFib (a,b,0)) * (Fib ($1 -' 1))) + ((GenFib (a,b,1)) * (Fib $1));
GenFib (a,b,1) = ((GenFib (a,b,0)) * (Fib 0)) + ((GenFib (a,b,1)) * (Fib 1)) by PRE_FF:1
.= ((GenFib (a,b,0)) * (Fib (1 -' 1))) + ((GenFib (a,b,1)) * (Fib 1)) by XREAL_1:232 ;
then A1: S₁[1] ;
A2: for k being non zero Nat st S₁[k] & S₁[k + 1] holds
S₁[k + 2]

proof

let k be non zero Nat; :: thesis: ( S₁[k] & S₁[k + 1] implies S₁[k + 2] )
assume that
A3: S₁[k] and
A4: S₁[k + 1] ; :: thesis: S₁[k + 2]
1 <= k by NAT_2:19;
then A5: (Fib (k -' 1)) + (Fib ((k + 1) -' 1)) = (Fib (k -' 1)) + (Fib ((k -' 1) + 1)) by NAT_D:38
.= Fib (((k -' 1) + 1) + 1) by PRE_FF:1
.= Fib ((k -' 1) + 2)
.= Fib ((k + 2) -' 1) by Th4 ;
GenFib (a,b,(k + 2)) = (((GenFib (a,b,0)) * (Fib (k -' 1))) + ((GenFib (a,b,1)) * (Fib k))) + (GenFib (a,b,(k + 1))) by A3, Th34
.= ((a * (Fib (k -' 1))) + ((GenFib (a,b,1)) * (Fib k))) + (GenFib (a,b,(k + 1))) by Th32
.= ((a * (Fib (k -' 1))) + (b * (Fib k))) + (GenFib (a,b,(k + 1))) by Th32
.= (((a * (Fib (k -' 1))) + (b * (Fib k))) + ((GenFib (a,b,0)) * (Fib ((k + 1) -' 1)))) + ((GenFib (a,b,1)) * (Fib (k + 1))) by A4
.= (((a * (Fib (k -' 1))) + (b * (Fib k))) + (a * (Fib ((k + 1) -' 1)))) + ((GenFib (a,b,1)) * (Fib (k + 1))) by Th32
.= (((a * (Fib (k -' 1))) + (b * (Fib k))) + (a * (Fib ((k + 1) -' 1)))) + (b * (Fib (k + 1))) by Th32
.= (a * ((Fib (k -' 1)) + (Fib ((k + 1) -' 1)))) + (b * ((Fib k) + (Fib (k + 1))))
.= (a * (Fib ((k + 2) -' 1))) + (b * (Fib (k + 2))) by A5, FIB_NUM2:24
.= (a * (Fib ((k + 2) -' 1))) + ((GenFib (a,b,1)) * (Fib (k + 2))) by Th32
.= ((GenFib (a,b,0)) * (Fib ((k + 2) -' 1))) + ((GenFib (a,b,1)) * (Fib (k + 2))) by Th32 ;
hence S₁[k + 2] ; :: thesis: verum

end;

(0 + 1) + 1 = 2 ;
then A6: Fib 2 = 1 by PRE_FF:1;
GenFib (a,b,2) = GenFib (a,b,(0 + 2))
.= ((GenFib (a,b,0)) * (Fib (1 + 0))) + ((GenFib (a,b,1)) * (Fib 2)) by A6, Th34, PRE_FF:1
.= ((GenFib (a,b,0)) * (Fib (1 + (1 -' 1)))) + ((GenFib (a,b,1)) * (Fib 2)) by XREAL_1:232
.= ((GenFib (a,b,0)) * (Fib ((1 + 1) -' 1))) + ((GenFib (a,b,1)) * (Fib 2)) by NAT_D:38
.= ((GenFib (a,b,0)) * (Fib (2 -' 1))) + ((GenFib (a,b,1)) * (Fib 2)) ;
then A7: S₁[2] ;
for k being non zero Nat holds S₁[k] from FIB_NUM2:sch 1(A1, A7, A2);
hence GenFib (a,b,n) = ((GenFib (a,b,0)) * (Fib (n -' 1))) + ((GenFib (a,b,1)) * (Fib n)) ; :: thesis: verum

end;