:: deftheorem Def1 defines EXP NAT_5:def 1 :
for k being natural Number
for b₂ being sequence of NAT holds
( b₂ = EXP k iff for n being Nat holds b₂ . n = n |^ k );