:: deftheorem defines valid_power_output_pred NOMIN_6:def 9 :
for V, A being set
for z being Element of V
for b0 being Complex
for n0 being Nat
for d being object holds
( valid_power_output_pred A,z,b0,n0,d iff ex d1 being NonatomicND of V,A st
( d = d1 & z in dom d1 & d1 . z = b0 |^ n0 ) );