let nn, nn9, A, B, N be Nat; :: thesis: ( nn = 2 * nn9 & Fusc N = (A * (Fusc nn)) + (B * (Fusc (nn + 1))) implies Fusc N = ((A + B) * (Fusc nn9)) + (B * (Fusc (nn9 + 1))) )
assume that
A1: nn = 2 * nn9 and
A2: Fusc N = (A * (Fusc nn)) + (B * (Fusc (nn + 1))) ; :: thesis: Fusc N = ((A + B) * (Fusc nn9)) + (B * (Fusc (nn9 + 1)))
Fusc (nn + 1) = (Fusc nn9) + (Fusc (nn9 + 1)) by A1, Th17;
hence Fusc N = (A * (Fusc nn9)) + ((B * (Fusc nn9)) + (B * (Fusc (nn9 + 1)))) by A1, A2, Th17
.= ((A + B) * (Fusc nn9)) + (B * (Fusc (nn9 + 1))) ;
:: thesis: verum