:: deftheorem defines factorial_program NOMIN_5:def 13 :
for V, A being set
for loc being b₁ -valued Function
for val being Function
for z being Element of V holds factorial_program (A,loc,val,z) = PP_composition ((factorial_main_part (A,loc,val)),(SC_assignment ((denaming (V,A,(loc /. 4))),z)));