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