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₁[ Nat] means (GenFib a,b,$1) + (GenFib c,d,$1) = GenFib (a + c),(b + d),$1;
A1: for k being Nat st S₁[k] & S₁[k + 1] holds
S₁[k + 2]

proof

let k be Nat; :: thesis: ( S₁[k] & S₁[k + 1] implies S₁[k + 2] )
assume that
A2: S₁[k] and
A3: S₁[k + 1] ; :: thesis: S₁[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₁[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: S₁[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₁[ 0 ] ;
for k being Nat holds S₁[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