let a,

b,

n be

Nat;

(GenFib (a,b,n)) + (GenFib (a,b,(n + 1))) = GenFib (a,b,(n + 2))
(GenFib (a,b,n)) + (GenFib (a,b,(n + 1))) =

GenFib (

a,

b,

((n + 1) + 1))

by Th32
.=

GenFib (

a,

b,

(n + 2))
;

hence
(GenFib (

a,

b,

n))

+ (GenFib (a,b,(n + 1))) = GenFib (

a,

b,

(n + 2))
;

verum