let n, A, B, N be Nat; :: thesis: ( Fusc N = (A * (Fusc (2 * n))) + (B * (Fusc ((2 * n) + 1))) implies Fusc N = ((A + B) * (Fusc n)) + (B * (Fusc (n + 1))) )
assume A1: Fusc N = (A * (Fusc (2 * n))) + (B * (Fusc ((2 * n) + 1))) ; :: thesis: Fusc N = ((A + B) * (Fusc n)) + (B * (Fusc (n + 1)))
Fusc ((2 * n) + 1) = (Fusc n) + (Fusc (n + 1)) by Th15;
hence Fusc N = (A * (Fusc n)) + ((B * (Fusc n)) + (B * (Fusc (n + 1)))) by A1, Th15
.= ((A + B) * (Fusc n)) + (B * (Fusc (n + 1))) ;
:: thesis: verum