let a, b, n be Element of NAT ; :: thesis: GenFib b,(a + b),n = GenFib a,b,(n + 1)
defpred S₁[ Nat] means GenFib b,(a + b),$1 = GenFib a,b,($1 + 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 ( S₁[k] & S₁[k + 1] ) ; :: thesis: S₁[k + 2]
then GenFib b,(a + b),(k + 2) = (GenFib a,b,(k + 1)) + (GenFib a,b,(k + 2)) by Th34
.= GenFib a,b,(k + 3) by Th35
.= GenFib a,b,((k + 2) + 1) ;
hence S₁[k + 2] ; :: thesis: verum

end;

GenFib b,(a + b),0 = b by Th32
.= GenFib a,b,(0 + 1) by Th32 ;
then A2: S₁[ 0 ] ;
GenFib b,(a + b),1 = a + b by Th32
.= a + (GenFib a,b,1) by Th32
.= (GenFib a,b,0 ) + (GenFib a,b,(0 + 1)) by Th32
.= GenFib a,b,(0 + 2) by Th34
.= GenFib a,b,(1 + 1) ;
then A3: S₁[1] ;
for k being Nat holds S₁[k] from FIB_NUM:sch 1(A2, A3, A1);
hence GenFib b,(a + b),n = GenFib a,b,(n + 1) ; :: thesis: verum