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