let a, b, k, n be Element of NAT ; :: thesis: GenFib (GenFib a,b,k),(GenFib a,b,(k + 1)),n = GenFib a,b,(n + k)
defpred S₁[ Nat] means GenFib (GenFib a,b,k),(GenFib a,b,(k + 1)),$1 = GenFib a,b,($1 + k);
A1: S₁[1] by Th32;
A2: for i being Nat st S₁[i] & S₁[i + 1] holds
S₁[i + 2]

proof

let i be Nat; :: thesis: ( S₁[i] & S₁[i + 1] implies S₁[i + 2] )
assume ( S₁[i] & S₁[i + 1] ) ; :: thesis: S₁[i + 2]
then GenFib (GenFib a,b,k),(GenFib a,b,(k + 1)),(i + 2) = (GenFib a,b,(i + k)) + (GenFib a,b,((i + k) + 1)) by Th34
.= GenFib a,b,((i + k) + 2) by Th34
.= GenFib a,b,((i + 2) + k) ;
hence S₁[i + 2] ; :: thesis: verum

end;

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