defpred S_{1}[ Nat] means GenFib (2,1,$1) = Lucas $1;

A1: S_{1}[1]
by Th11, Th32;

A2: for k being Nat st S_{1}[k] & S_{1}[k + 1] holds

S_{1}[k + 2]
_{1}[ 0 ]
by Th11, Th32;

for k being Nat holds S_{1}[k]
from FIB_NUM:sch 1(A3, A1, A2);

hence for n being Element of NAT holds GenFib (2,1,n) = Lucas n ; :: thesis: verum

A1: S

A2: for k being Nat st S

S

proof

A3:
S
let k be Nat; :: thesis: ( S_{1}[k] & S_{1}[k + 1] implies S_{1}[k + 2] )

assume ( S_{1}[k] & S_{1}[k + 1] )
; :: thesis: S_{1}[k + 2]

then GenFib (2,1,(k + 2)) = (Lucas k) + (Lucas (k + 1)) by Th34

.= Lucas (k + 2) by Th12 ;

hence S_{1}[k + 2]
; :: thesis: verum

end;assume ( S

then GenFib (2,1,(k + 2)) = (Lucas k) + (Lucas (k + 1)) by Th34

.= Lucas (k + 2) by Th12 ;

hence S

for k being Nat holds S

hence for n being Element of NAT holds GenFib (2,1,n) = Lucas n ; :: thesis: verum