defpred S₁[ Nat] means GenFib (2,1,$1) = Lucas $1;
A1: S₁[1] by Th11, Th32;
A2: 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 (2,1,(k + 2)) = (Lucas k) + (Lucas (k + 1)) by Th34
.= Lucas (k + 2) by Th12 ;
hence S₁[k + 2] ; :: thesis: verum

end;

A3: S₁[ 0 ] by Th11, Th32;
for k being Nat holds S₁[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