let a, b, n be Element of NAT ; :: thesis: GenFib (a,b,(n + 1)) = (a * (Fib n)) + (b * (Fib (n + 1)))

defpred S_{1}[ 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:24, 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}[1]
by A1, PRE_FF:1;

A3: for k being Nat st S_{1}[k] & S_{1}[k + 1] holds

S_{1}[k + 2]
_{1}[ 0 ]
by Th32, PRE_FF:1;

for k being Nat holds S_{1}[k]
from FIB_NUM:sch 1(A6, A2, A3);

hence GenFib (a,b,(n + 1)) = (a * (Fib n)) + (b * (Fib (n + 1))) ; :: thesis: verum

defpred S

A1: Fib 2 = Fib (0 + 2)

.= 0 + 1 by FIB_NUM2:24, 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

A3: for k being Nat st S

S

proof

A6:
S
let k be Nat; :: thesis: ( S_{1}[k] & S_{1}[k + 1] implies S_{1}[k + 2] )

assume that

A4: S_{1}[k]
and

A5: S_{1}[k + 1]
; :: thesis: S_{1}[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:24

.= (a * (Fib (k + 2))) + (b * (Fib ((k + 1) + 2))) by FIB_NUM2:24

.= (a * (Fib (k + 2))) + (b * (Fib ((k + 2) + 1))) ;

hence S_{1}[k + 2]
; :: thesis: verum

end;assume that

A4: S

A5: S

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

.= (a * (Fib (k + 2))) + (b * (Fib ((k + 1) + 2))) by FIB_NUM2:24

.= (a * (Fib (k + 2))) + (b * (Fib ((k + 2) + 1))) ;

hence S

for k being Nat holds S

hence GenFib (a,b,(n + 1)) = (a * (Fib n)) + (b * (Fib (n + 1))) ; :: thesis: verum