:: deftheorem defines factorial_loop_body NOMIN_5:def 9 :
for V, A being set
for loc being b₁ -valued Function holds factorial_loop_body (A,loc) = PP_composition ((SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))),(SC_assignment ((multiplication (A,(loc /. 4),(loc /. 1))),(loc /. 4))));