:: deftheorem Def12 defines FPower POLYNOM5:def 12 :
for L being non empty unital multMagma
for x being Element of L
for n being Nat
for b₄ being Function of L,L holds
( b₄ = FPower (x,n) iff for y being Element of L holds b₄ . y = x * (power (y,n)) );