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);
A1: S1[ 0 ]
proof
2 * (Fib n) = GenFib 0 ,2,n
proof
defpred S2[ Nat] means 2 * (Fib $1) = GenFib 0 ,2,$1;
A2: S2[ 0 ] by Th32, PRE_FF:1;
A3: S2[1] by Th32, PRE_FF:1;
A4: 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 that
A5: S2[i] and
A6: 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 A5, A6, Th34 ;
hence S2[i + 2] ; :: thesis: verum
end;
for i being Nat holds S2[i] from FIB_NUM:sch 1(A2, A3, A4);
 hence 2 * (Fib n) = GenFib 0 ,2,n ; :: thesis: verum
end;
hence S1[ 0 ] by Th11, PRE_FF:1; :: thesis: verum
end;
A7: S1[1]
proof
(Lucas n) + (Fib n) = GenFib 0 ,2,(n + 1)
proof
defpred S2[ Nat] means (Lucas $1) + (Fib $1) = GenFib 0 ,2,($1 + 1);
A8: S2[ 0 ] by Th11, Th32, PRE_FF:1;
A9: S2[1]
proof
(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) ;
hence S2[1] ; :: thesis: verum
end;
A10: 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 that
A11: S2[j] and
A12: 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 A11, A12
.= GenFib 0 ,2,(j + 3) by Th35
.= GenFib 0 ,2,((j + 2) + 1) ;
hence S2[j + 2] ; :: thesis: verum
end;
for j being Nat holds S2[j] from FIB_NUM:sch 1(A8, A9, A10);
 hence (Lucas n) + (Fib n) = GenFib 0 ,2,(n + 1) ; :: thesis: verum
end;
hence S1[1] by Th11, PRE_FF:1; :: thesis: verum
end;
A13: 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 that
A14: S1[k] and
A15: 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 A14, A15, 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(A1, A7, A13);
 hence ((Fib m) * (Lucas n)) + ((Lucas m) * (Fib n)) = GenFib (Fib 0 ),(Lucas 0 ),(n + m) ; :: thesis: verum