:: deftheorem defines valid_power_input_pred NOMIN_6:def 7 :
for V, A being set
for val being Function
for b0 being Complex
for n0 being Nat
for d being object holds
( valid_power_input_pred V,A,val,b0,n0,d iff ex d1 being NonatomicND of V,A st
( d = d1 & {(val . 1),(val . 2),(val . 3),(val . 4),(val . 5)} c= dom d1 & d1 . (val . 1) = 0 & d1 . (val . 2) = 1 & d1 . (val . 3) = b0 & d1 . (val . 4) = n0 & d1 . (val . 5) = 1 ) );