let k be Nat; :: thesis: #divs (2 |^ k) = k + 1
2 is Prime by INT_2:28;
then card (NatDivisors (2 |^ k)) = k + 1 by CardNatDiv;
hence #divs (2 |^ k) = k + 1 by ThDivs; :: thesis: verum