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 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; :: thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
A2: S1[k] and
A3: S1[k + 1] ; :: thesis: 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 ;
hence S1[k + 2] ; :: thesis: 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 ;
(
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) ; :: thesis: verum