theorem Th8: :: NOMIN_5:8

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