:: deftheorem defines factorial_var_init NOMIN_5:def 11 :
for V, A being set
for loc being b₁ -valued Function
for val being Function holds factorial_var_init (A,loc,val) = PP_composition ((SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1))),(SC_assignment ((denaming (V,A,(val . 2))),(loc /. 2))),(SC_assignment ((denaming (V,A,(val . 3))),(loc /. 3))),(SC_assignment ((denaming (V,A,(val . 4))),(loc /. 4))));