:: deftheorem Def12 defines power_inv NOMIN_6:def 12 :
for V, A being set
for loc being b₁ -valued Function
for b0 being Complex
for n0 being Nat
for b₆ being SCPartialNominativePredicate of V,A holds
( b₆ = power_inv (A,loc,b0,n0) iff ( dom b₆ = ND (V,A) & ( for d being object st d in dom b₆ holds
( ( power_inv_pred A,loc,b0,n0,d implies b₆ . d = TRUE ) & ( not power_inv_pred A,loc,b0,n0,d implies b₆ . d = FALSE ) ) ) ) );