:: deftheorem Def3 defines #Z PREPOWER:def 3 :
for a being Real
for k being Integer holds
( ( k >= 0 implies a #Z k = a |^ |.k.| ) & ( k < 0 implies a #Z k = (a |^ |.k.|) " ) );