let a, b, c, d, n be Element of NAT ; :: thesis: (GenFib (a,b,n)) + (GenFib (c,d,n)) = GenFib ((a + c),(b + d),n)

defpred S_{1}[ Nat] means (GenFib (a,b,$1)) + (GenFib (c,d,$1)) = GenFib ((a + c),(b + d),$1);

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

S_{1}[k + 2]

.= b + d by Th32

.= GenFib ((a + c),(b + d),1) by Th32 ;

then A4: S_{1}[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: S_{1}[ 0 ]
;

for k being Nat holds S_{1}[k]
from FIB_NUM:sch 1(A5, A4, A1);

hence (GenFib (a,b,n)) + (GenFib (c,d,n)) = GenFib ((a + c),(b + d),n) ; :: thesis: verum

defpred S

A1: for k being Nat st S

S

proof

(GenFib (a,b,1)) + (GenFib (c,d,1)) =
b + (GenFib (c,d,1))
by Th32
let k be Nat; :: thesis: ( S_{1}[k] & S_{1}[k + 1] implies S_{1}[k + 2] )

assume that

A2: S_{1}[k]
and

A3: S_{1}[k + 1]
; :: thesis: S_{1}[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 S_{1}[k + 2]
; :: thesis: verum

end;assume that

A2: S

A3: S

(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 S

.= b + d by Th32

.= GenFib ((a + c),(b + d),1) by Th32 ;

then A4: S

(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: S

for k being Nat holds S

hence (GenFib (a,b,n)) + (GenFib (c,d,n)) = GenFib ((a + c),(b + d),n) ; :: thesis: verum