theorem :: ASYMPT_1:53

4 to_power 4 = 256 by Lm37;