let n, m be Nat; :: thesis: ((Fib m) * (Lucas n)) + ((Lucas m) * (Fib n)) = GenFib (Fib 0 ),(Lucas 0 ),(n + m)
defpred S1[ Nat] means ((Fib $1) * (Lucas n)) + ((Lucas $1) * (Fib n)) = GenFib (Fib 0 ),(Lucas 0 ),(n + $1);
2 * (Fib n) = GenFib 0 ,2,n
proof
defpred S2[ Nat] means 2 * (Fib $1) = GenFib 0 ,2,$1;
A1: S2[1] by Th32, PRE_FF:1;
A2: for i being Nat st S2[i] & S2[i + 1] holds
S2[i + 2]
proof
let i be Nat; :: thesis: ( S2[i] & S2[i + 1] implies S2[i + 2] )
assume A3: ( S2[i] & S2[i + 1] ) ; :: thesis: S2[i + 2]
2 * (Fib (i + 2)) = 2 * ((Fib i) + (Fib (i + 1))) by FIB_NUM2:26
.= (2 * (Fib i)) + (2 * (Fib (i + 1)))
.= GenFib 0 ,2,(i + 2) by A3, Th34 ;
hence S2[i + 2] ; :: thesis: verum
end;
A4: S2[ 0 ] by Th32, PRE_FF:1;
for i being Nat holds S2[i] from FIB_NUM:sch 1(A4, A1, A2);
 hence 2 * (Fib n) = GenFib 0 ,2,n ; :: thesis: verum
end;
then A5: S1[ 0 ] by Th11, PRE_FF:1;
(Lucas n) + (Fib n) = GenFib 0 ,2,(n + 1)
proof
defpred S2[ Nat] means (Lucas $1) + (Fib $1) = GenFib 0 ,2,($1 + 1);
A6: for j being Nat st S2[j] & S2[j + 1] holds
S2[j + 2]
proof
let j be Nat; :: thesis: ( S2[j] & S2[j + 1] implies S2[j + 2] )
assume A7: ( S2[j] & S2[j + 1] ) ; :: thesis: S2[j + 2]
(Lucas (j + 2)) + (Fib (j + 2)) = ((Lucas j) + (Lucas (j + 1))) + (Fib (j + 2)) by Th12
.= ((Lucas j) + (Lucas (j + 1))) + ((Fib j) + (Fib (j + 1))) by FIB_NUM2:26
.= (GenFib 0 ,2,(j + 1)) + (GenFib 0 ,2,(j + 2)) by A7
.= GenFib 0 ,2,(j + 3) by Th35
.= GenFib 0 ,2,((j + 2) + 1) ;
hence S2[j + 2] ; :: thesis: verum
end;
(Lucas 1) + (Fib 1) = 0 + (GenFib 0 ,2,1) by Th11, Th32, PRE_FF:1
.= (GenFib 0 ,2,(0 + 0 )) + (GenFib 0 ,2,(0 + 1)) by Th32
.= GenFib 0 ,2,(0 + 2) by Th34
.= GenFib 0 ,2,(1 + 1) ;
then A8: S2[1] ;
A9: S2[ 0 ] by Th11, Th32, PRE_FF:1;
for j being Nat holds S2[j] from FIB_NUM:sch 1(A9, A8, A6);
 hence (Lucas n) + (Fib n) = GenFib 0 ,2,(n + 1) ; :: thesis: verum
end;
then A10: S1[1] by Th11, PRE_FF:1;
A11: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; :: thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume A12: ( S1[k] & S1[k + 1] ) ; :: thesis: S1[k + 2]
((Fib (k + 2)) * (Lucas n)) + ((Lucas (k + 2)) * (Fib n)) = (((Fib k) + (Fib (k + 1))) * (Lucas n)) + ((Lucas (k + 2)) * (Fib n)) by FIB_NUM2:26
.= (((Fib k) * (Lucas n)) + ((Fib (k + 1)) * (Lucas n))) + (((Lucas k) + (Lucas (k + 1))) * (Fib n)) by Th12
.= (GenFib 0 ,2,(n + k)) + (GenFib 0 ,2,((n + k) + 1)) by A12, Th11, PRE_FF:1
.= GenFib 0 ,2,((n + k) + 2) by Th34
.= GenFib (Fib 0 ),(Lucas 0 ),(n + (k + 2)) by Th11, PRE_FF:1 ;
hence S1[k + 2] ; :: thesis: verum
end;
for k being Nat holds S1[k] from FIB_NUM:sch 1(A5, A10, A11);
 hence ((Fib m) * (Lucas n)) + ((Lucas m) * (Fib n)) = GenFib (Fib 0 ),(Lucas 0 ),(n + m) ; :: thesis: verum