:: deftheorem defines |^ MESFUNC7:def 3 :
for x being Element of ExtREAL
for k being Nat holds x |^ k = Product (k |-> x);