:: deftheorem defines power_loop_body NOMIN_6:def 2 :
for V, A being set
for loc being b₁ -valued Function holds power_loop_body (A,loc) = PP_composition ((SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))),(SC_assignment ((multiplication (A,(loc /. 5),(loc /. 3))),(loc /. 5))));