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