for V, A being set
for z being Element of V
for loc being b₁ -valued Function
for val being Function
for n0 being Nat
for b0 being Complex st not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4,loc /. 5 are_mutually_distinct & loc,val are_compatible_wrt_5_locs & ( for T being TypeSCNominativeData of V,A holds loc /. 1 is_a_value_on T ) & ( for T being TypeSCNominativeData of V,A holds loc /. 4 is_a_value_on T ) holds
<*(valid_power_input (V,A,val,b0,n0)),(power_program (A,loc,val,z)),(valid_power_output (A,z,b0,n0))*> is SFHT of (ND (V,A))