theorem Th9: :: NOMIN_5:9

for V, A being set
for loc being b₁ -valued Function
for n0 being Nat st not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4 are_mutually_distinct holds
<*(factorial_inv (A,loc,n0)),(factorial_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))*> is SFHT of (ND (V,A))