let a, b, n be Element of NAT ; (GenFib a,b,n) + (GenFib a,b,(n + 4)) = 3 * (GenFib a,b,(n + 2))
(GenFib a,b,n) + (GenFib a,b,(n + 4)) =
(GenFib a,b,n) + ((GenFib a,b,(n + 2)) + (GenFib a,b,(n + 3)))
by Th36
.=
((GenFib a,b,n) + (GenFib a,b,(n + 2))) + (GenFib a,b,(n + 3))
.=
((GenFib a,b,n) + (GenFib a,b,(n + 2))) + ((GenFib a,b,(n + 1)) + (GenFib a,b,(n + 2)))
by Th35
.=
(((GenFib a,b,n) + (GenFib a,b,(n + 1))) + (GenFib a,b,(n + 2))) + (GenFib a,b,(n + 2))
.=
((GenFib a,b,(n + 2)) + (GenFib a,b,(n + 2))) + (GenFib a,b,(n + 2))
by Th34
.=
3 * (GenFib a,b,(n + 2))
;
hence
(GenFib a,b,n) + (GenFib a,b,(n + 4)) = 3 * (GenFib a,b,(n + 2))
; verum