theorem Th5: :: NOMIN_6:5

for V, A being set
for loc being b₁ -valued 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 holds
<*(power_inv (A,loc,b0,n0)),(power_loop_body (A,loc)),(power_inv (A,loc,b0,n0))*> is SFHT of (ND (V,A))