:: deftheorem defines Lucas_loop_body NOMIN_9:def 5 :
for V, A being set
for loc being b₁ -valued Function holds Lucas_loop_body (A,loc) = PP_composition ((SC_assignment ((denaming (V,A,(loc /. 4))),(loc /. 6))),(SC_assignment ((denaming (V,A,(loc /. 5))),(loc /. 4))),(SC_assignment ((multiplication (A,(loc /. 7),(loc /. 4))),(loc /. 9))),(SC_assignment ((multiplication (A,(loc /. 8),(loc /. 6))),(loc /. 10))),(SC_assignment ((subtraction (A,(loc /. 9),(loc /. 10))),(loc /. 5))),(SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))));