:: deftheorem Def8 defines valid_power_input NOMIN_6:def 8 :
for V, A being set
for val being Function
for b0 being Complex
for n0 being Nat
for b₆ being SCPartialNominativePredicate of V,A holds
( b₆ = valid_power_input (V,A,val,b0,n0) iff ( dom b₆ = ND (V,A) & ( for d being object st d in dom b₆ holds
( ( valid_power_input_pred V,A,val,b0,n0,d implies b₆ . d = TRUE ) & ( not valid_power_input_pred V,A,val,b0,n0,d implies b₆ . d = FALSE ) ) ) ) );