let a, b, c, d, n be Element of NAT ; (GenFib (a,b,n)) + (GenFib (c,d,n)) = GenFib ((a + c),(b + d),n)
defpred S1[ Nat] means (GenFib (a,b,$1)) + (GenFib (c,d,$1)) = GenFib ((a + c),(b + d),$1);
A1:
for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be
Nat;
( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that A2:
S1[
k]
and A3:
S1[
k + 1]
;
S1[k + 2]
(GenFib (a,b,(k + 2))) + (GenFib (c,d,(k + 2))) =
((GenFib (a,b,k)) + (GenFib (a,b,(k + 1)))) + (GenFib (c,d,(k + 2)))
by Th34
.=
((GenFib (a,b,k)) + (GenFib (a,b,(k + 1)))) + ((GenFib (c,d,k)) + (GenFib (c,d,(k + 1))))
by Th34
.=
(GenFib ((a + c),(b + d),k)) + ((GenFib (a,b,(k + 1))) + (GenFib (c,d,(k + 1))))
by A2
.=
GenFib (
(a + c),
(b + d),
(k + 2))
by A3, Th34
;
hence
S1[
k + 2]
;
verum
end;
(GenFib (a,b,1)) + (GenFib (c,d,1)) =
b + (GenFib (c,d,1))
by Th32
.=
b + d
by Th32
.=
GenFib ((a + c),(b + d),1)
by Th32
;
then A4:
S1[1]
;
(GenFib (a,b,0)) + (GenFib (c,d,0)) =
a + (GenFib (c,d,0))
by Th32
.=
a + c
by Th32
.=
GenFib ((a + c),(b + d),0)
by Th32
;
then A5:
S1[ 0 ]
;
for k being Nat holds S1[k]
from FIB_NUM:sch 1(A5, A4, A1);
hence
(GenFib (a,b,n)) + (GenFib (c,d,n)) = GenFib ((a + c),(b + d),n)
; verum