theorem :: PRE_FF:20

for n, A, B, N being Nat st Fusc N = (A * (Fusc (2 * n))) + (B * (Fusc ((2 * n) + 1))) holds
Fusc N = ((A + B) * (Fusc n)) + (B * (Fusc (n + 1)))