theorem Th11: :: NOMIN_6:11

for V, A being set
for z being Element of V
for loc being b₁ -valued Function
for n0 being Nat
for b0 being Complex st ( 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
<*(PP_inversion (PP_and ((Equality (A,(loc /. 1),(loc /. 4))),(power_inv (A,loc,b0,n0))))),(SC_assignment ((denaming (V,A,(loc /. 5))),z)),(valid_power_output (A,z,b0,n0))*> is SFHT of (ND (V,A))