:: deftheorem Def2 defines -powerfunc_of CARD_5:def 2 :
for M, N being Cardinal
for b₃ being Cardinal-Function holds
( b₃ = N -powerfunc_of M iff ( ( for x being object holds
( x in dom b₃ iff ( x in M & x is Cardinal ) ) ) & ( for K being Cardinal st K in M holds
b₃ . K = exp (K,N) ) ) );