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