:: deftheorem defines factorial_main_part NOMIN_5:def 12 :
for V, A being set
for loc being b₁ -valued Function
for val being Function holds factorial_main_part (A,loc,val) = PP_composition ((factorial_var_init (A,loc,val)),(factorial_main_loop (A,loc)));