defpred S₁[ Nat] means 2 * (Fib ((2 * $1) + 1)) = ((Lucas ($1 + 1)) * (Fib $1)) + ((Lucas $1) * (Fib ($1 + 1)));
(0 + 1) + 1 = 2 ;
then A1: Fib 2 = 1 by PRE_FF:1;
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 that
A3: S₁[k] and
A4: S₁[k + 1] ; :: thesis: S₁[k + 2]
set f2 = Fib (k + 2);
set f1 = Fib (k + 1);
set f = Fib k;
set l2 = Lucas (k + 2);
set l1 = Lucas (k + 1);
set l = Lucas k;
A5: 2 * (Fib (2 * k)) = 2 * ((Fib ((2 * k) + 2)) - (Fib ((2 * k) + 1))) by FIB_NUM2:30
.= 2 * ((Fib (((2 * k) + 1) + 1)) - (Fib ((2 * k) + 1)))
.= 2 * (((Fib (((2 * k) + 1) + 2)) - (Fib ((2 * k) + 1))) - (Fib ((2 * k) + 1))) by FIB_NUM2:29
.= (2 * (Fib ((2 * k) + 3))) - (2 * (2 * (Fib ((2 * k) + 1))))
.= (((Lucas (k + 2)) * (Fib (k + 1))) + ((Lucas (k + 1)) * (Fib (k + 2)))) - (2 * (((Lucas (k + 1)) * (Fib k)) + ((Lucas k) * (Fib (k + 1))))) by A3, A4
.= ((((Lucas (k + 2)) * (Fib (k + 1))) + ((Lucas (k + 1)) * (Fib (k + 2)))) - ((2 * (Lucas (k + 1))) * (Fib k))) - ((2 * (Lucas k)) * (Fib (k + 1)))
.= (((((Lucas k) + (Lucas (k + 1))) * (Fib (k + 1))) + ((Lucas (k + 1)) * (Fib (k + 2)))) - ((2 * (Lucas (k + 1))) * (Fib k))) - ((2 * (Lucas k)) * (Fib (k + 1))) by Th12
.= (((((Lucas k) * (Fib (k + 1))) + ((Lucas (k + 1)) * (Fib (k + 1)))) + ((Lucas (k + 1)) * ((Fib k) + (Fib (k + 1))))) - ((2 * (Lucas (k + 1))) * (Fib k))) - ((2 * (Lucas k)) * (Fib (k + 1))) by FIB_NUM2:24
.= (((2 * (Lucas (k + 1))) * (Fib (k + 1))) - ((Lucas k) * (Fib (k + 1)))) - ((Lucas (k + 1)) * (Fib k)) ;
2 * (Fib ((2 * (k + 2)) + 1)) = 2 * (Fib (((2 * k) + 3) + 2))
.= 2 * ((Fib ((2 * k) + 3)) + (Fib (((2 * k) + 3) + 1))) by FIB_NUM2:24
.= 2 * ((Fib ((2 * k) + 3)) + (Fib (((2 * k) + 2) + 2)))
.= 2 * ((Fib ((2 * k) + 3)) + ((Fib ((2 * k) + 2)) + (Fib (((2 * k) + 2) + 1)))) by FIB_NUM2:24
.= 2 * (((Fib ((2 * k) + 3)) + (Fib (((2 * k) + 1) + 1))) + (Fib ((2 * k) + 3)))
.= 2 * (((Fib ((2 * k) + 3)) + ((Fib (((2 * k) + 1) + 2)) - (Fib ((2 * k) + 1)))) + (Fib ((2 * k) + 3))) by FIB_NUM2:29
.= (3 * (2 * (Fib ((2 * k) + 3)))) - (2 * (Fib ((2 * k) + 1)))
.= (3 * (((Lucas (k + 2)) * (Fib (k + 1))) + ((Lucas (k + 1)) * (Fib (k + 2))))) - (2 * (Fib ((2 * k) + 1))) by A4
.= ((((3 * (Lucas (k + 2))) * (Fib (k + 1))) + ((3 * (Lucas (k + 1))) * (Fib (k + 2)))) - ((Lucas (k + 1)) * (Fib k))) - ((Lucas k) * (Fib (k + 1))) by A3
.= ((((3 * ((Lucas k) + (Lucas (k + 1)))) * (Fib (k + 1))) + ((3 * (Lucas (k + 1))) * (Fib (k + 2)))) - ((Lucas (k + 1)) * (Fib k))) - ((Lucas k) * (Fib (k + 1))) by Th12
.= (((((3 * (Lucas k)) + (3 * (Lucas (k + 1)))) * (Fib (k + 1))) + ((3 * (Lucas (k + 1))) * ((Fib k) + (Fib (k + 1))))) - ((Lucas (k + 1)) * (Fib k))) - ((Lucas k) * (Fib (k + 1))) by FIB_NUM2:24
.= ((((3 * (Lucas k)) * (Fib (k + 1))) + ((4 * (Lucas (k + 1))) * (Fib (k + 1)))) + ((3 * (Lucas (k + 1))) * (Fib k))) + ((((2 * (Lucas (k + 1))) * (Fib (k + 1))) - ((Lucas k) * (Fib (k + 1)))) - ((Lucas (k + 1)) * (Fib k)))
.= ((((3 * (Lucas k)) * (Fib (k + 1))) + ((4 * (Lucas (k + 1))) * (Fib (k + 1)))) + ((3 * (Lucas (k + 1))) * (Fib k))) + (2 * ((Lucas k) * (Fib k))) by A5, Th28
.= (((((((Lucas k) * (Fib (k + 1))) + ((Lucas (k + 1)) * (Fib (k + 1)))) + ((Lucas (k + 1)) * ((Fib k) + (Fib (k + 1))))) + ((2 * (Lucas k)) * (Fib k))) + ((2 * (Lucas k)) * (Fib (k + 1)))) + ((2 * (Lucas (k + 1))) * (Fib k))) + ((2 * (Lucas (k + 1))) * (Fib (k + 1)))
.= (((((((Lucas k) + (Lucas (k + 1))) * (Fib (k + 1))) + ((Lucas (k + 1)) * (Fib (k + 2)))) + ((2 * (Lucas k)) * (Fib k))) + ((2 * (Lucas k)) * (Fib (k + 1)))) + ((2 * (Lucas (k + 1))) * (Fib k))) + ((2 * (Lucas (k + 1))) * (Fib (k + 1))) by FIB_NUM2:24
.= ((((((Lucas (k + 2)) * (Fib (k + 1))) + ((Lucas (k + 1)) * (Fib (k + 2)))) + ((2 * (Lucas k)) * (Fib k))) + ((2 * (Lucas k)) * (Fib (k + 1)))) + ((2 * (Lucas (k + 1))) * (Fib k))) + ((2 * (Lucas (k + 1))) * (Fib (k + 1))) by Th12
.= (((Lucas (k + 2)) * (Fib (k + 1))) + ((Lucas (k + 1)) * (Fib (k + 2)))) + (2 * (((((Lucas k) * (Fib k)) + ((Lucas k) * (Fib (k + 1)))) + ((Lucas (k + 1)) * (Fib k))) + ((Lucas (k + 1)) * (Fib (k + 1)))))
.= (2 * (Fib ((2 * k) + 3))) + (2 * (((((Lucas k) * (Fib k)) + ((Lucas k) * (Fib (k + 1)))) + ((Lucas (k + 1)) * (Fib k))) + ((Lucas (k + 1)) * (Fib (k + 1))))) by A4
.= 2 * ((Fib ((2 * k) + 3)) + (((Lucas k) + (Lucas (k + 1))) * ((Fib k) + (Fib (k + 1)))))
.= 2 * ((Fib ((2 * k) + 3)) + (((Lucas k) + (Lucas (k + 1))) * (Fib (k + 2)))) by FIB_NUM2:24
.= 2 * ((Fib ((2 * k) + 3)) + ((Lucas (k + 2)) * (Fib (k + 2)))) by Th12
.= ((2 * (Fib ((2 * k) + 3))) + ((Lucas (k + 2)) * (Fib (k + 2)))) + ((Lucas (k + 2)) * (Fib (k + 2)))
.= ((((Lucas (k + 1)) * (Fib (k + 2))) + ((Lucas (k + 2)) * (Fib (k + 1)))) + ((Lucas (k + 2)) * (Fib (k + 2)))) + ((Lucas (k + 2)) * (Fib (k + 2))) by A4
.= (((Lucas (k + 1)) + (Lucas (k + 2))) * (Fib (k + 2))) + ((Lucas (k + 2)) * ((Fib (k + 1)) + (Fib (k + 2))))
.= (((Lucas (k + 1)) + (Lucas ((k + 1) + 1))) * (Fib (k + 2))) + ((Lucas (k + 2)) * (Fib ((k + 1) + 2))) by FIB_NUM2:24
.= ((Lucas ((k + 2) + 1)) * (Fib (k + 2))) + ((Lucas (k + 2)) * (Fib ((k + 2) + 1))) by Th12 ;
hence S₁[k + 2] ; :: thesis: verum

end;

(1 + 1) + 1 = 3 ;
then 2 * (Fib ((2 * 1) + 1)) = 2 * 2 by A1, PRE_FF:1
.= ((Lucas (1 + 1)) * (Fib 1)) + ((Lucas 1) * (Fib (1 + 1))) by A1, Th11, Th14, PRE_FF:1 ;
then A6: S₁[1] ;
A7: S₁[ 0 ] by Th11, PRE_FF:1;
for k being Nat holds S₁[k] from FIB_NUM:sch 1(A7, A6, A2);
hence for n being Element of NAT holds 2 * (Fib ((2 * n) + 1)) = ((Lucas (n + 1)) * (Fib n)) + ((Lucas n) * (Fib (n + 1))) ; :: thesis: verum