theorem Th6: :: NOMIN_6:6

for V, A being set
for loc being b₁ -valued Function
for n0 being Nat
for b0 being Complex holds <*(PP_inversion (power_inv (A,loc,b0,n0))),(power_loop_body (A,loc)),(power_inv (A,loc,b0,n0))*> is SFHT of (ND (V,A))