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:24
.= (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:24
.= (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:24
.= (((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