:: deftheorem defpower defines -power FIELD_16:def 4 :
for n, m being Nat holds
( m is n -power iff ex l being non zero Nat st m = n |^ l );