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: S₁[ 0 ]

proof

GenFib b,(a + b),0 = b by Th32
.= GenFib a,b,(0 + 1) by Th32 ;
hence S₁[ 0 ] ; :: thesis: verum

end;

A2: S₁[1]

proof

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) ;
hence S₁[1] ; :: thesis: verum

end;

A3: 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
A4: S₁[k] and
A5: S₁[k + 1] ; :: thesis: S₁[k + 2]
GenFib b,(a + b),(k + 2) = (GenFib a,b,(k + 1)) + (GenFib a,b,(k + 2)) by A4, A5, Th34
.= GenFib a,b,(k + 3) by Th35
.= GenFib a,b,((k + 2) + 1) ;
hence S₁[k + 2] ; :: thesis: verum

end;

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