set L = Lucas_Sequence (0,1,1,(- 1));
set F = Fib ;
( dom Fib = NAT & dom (Lucas_Sequence (0,1,1,(- 1))) = NAT ) by FUNCT_2:def 1;
hence dom (Lucas_Sequence (0,1,1,(- 1))) = dom Fib ; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (Lucas_Sequence (0,1,1,(- 1))) or (Lucas_Sequence (0,1,1,(- 1))) . b₁ = Fib . b₁ )
let n be object ; :: thesis: ( not n in dom (Lucas_Sequence (0,1,1,(- 1))) or (Lucas_Sequence (0,1,1,(- 1))) . n = Fib . n )
assume A1: n in dom (Lucas_Sequence (0,1,1,(- 1))) ; :: thesis: (Lucas_Sequence (0,1,1,(- 1))) . n = Fib . n
defpred S₁[ Nat] means (Lucas_Sequence (0,1,1,(- 1))) . $1 = Fib . $1;
(Lucas_Sequence (0,1,1,(- 1))) . 0 = [0,1] by Def3;
then A2: S₁[ 0 ] by PRE_FF:def 1;
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 (0,1,1,(- 1))) . (k + 1) = [(((Lucas_Sequence (0,1,1,(- 1))) . k) `2),((1 * (((Lucas_Sequence (0,1,1,(- 1))) . k) `2)) - ((- 1) * (((Lucas_Sequence (0,1,1,(- 1))) . k) `1)))] by Def3
.= [((Fib . k) `2),(((Fib . k) `1) + ((Fib . k) `2))] by A4
.= Fib . (k + 1) by PRE_FF:def 1 ; :: thesis: verum

end;

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