let a, b be Nat; :: thesis: Lucas_Sequence (a,b,1,(- 1)) = GenFib (a,b)
set L = Lucas_Sequence (a,b,1,(- 1));
set F = GenFib (a,b);
( dom (GenFib (a,b)) = NAT & dom (Lucas_Sequence (a,b,1,(- 1))) = NAT ) by FUNCT_2:def 1;
hence dom (Lucas_Sequence (a,b,1,(- 1))) = dom (GenFib (a,b)) ; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (Lucas_Sequence (a,b,1,(- 1))) or (Lucas_Sequence (a,b,1,(- 1))) . b₁ = (GenFib (a,b)) . b₁ )
let n be object ; :: thesis: ( not n in dom (Lucas_Sequence (a,b,1,(- 1))) or (Lucas_Sequence (a,b,1,(- 1))) . n = (GenFib (a,b)) . n )
assume A1: n in dom (Lucas_Sequence (a,b,1,(- 1))) ; :: thesis: (Lucas_Sequence (a,b,1,(- 1))) . n = (GenFib (a,b)) . n
defpred S₁[ Nat] means (Lucas_Sequence (a,b,1,(- 1))) . $1 = (GenFib (a,b)) . $1;
(Lucas_Sequence (a,b,1,(- 1))) . 0 = [a,b] by Def3;
then A2: S₁[ 0 ] by FIB_NUM3:def 3;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
thus (Lucas_Sequence (a,b,1,(- 1))) . (k + 1) = [(((Lucas_Sequence (a,b,1,(- 1))) . k) `2),((1 * (((Lucas_Sequence (a,b,1,(- 1))) . k) `2)) - ((- 1) * (((Lucas_Sequence (a,b,1,(- 1))) . k) `1)))] by Def3
.= [(((GenFib (a,b)) . k) `2),((((GenFib (a,b)) . k) `1) + (((GenFib (a,b)) . k) `2))] by A4
.= (GenFib (a,b)) . (k + 1) by FIB_NUM3:def 3 ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3);
hence (Lucas_Sequence (a,b,1,(- 1))) . n = (GenFib (a,b)) . n by A1; :: thesis: verum