:: deftheorem defines power_inv_pred NOMIN_6:def 11 :
for V, A being set
for loc being b₁ -valued Function
for b0 being Complex
for n0 being Nat
for d being object holds
( power_inv_pred A,loc,b0,n0,d iff ex d1 being NonatomicND of V,A st
( d = d1 & {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5)} c= dom d1 & d1 . (loc /. 2) = 1 & d1 . (loc /. 3) = b0 & d1 . (loc /. 4) = n0 & ex S being Complex ex I being Nat st
( I = d1 . (loc /. 1) & S = d1 . (loc /. 5) & S = b0 |^ I ) ) );