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