:: deftheorem defines Lucas_program NOMIN_9:def 8 :
for V, A being set
for loc being b₁ -valued Function
for val being Function
for z being Element of V holds Lucas_program (A,loc,val,z) = PP_composition ((Lucas_main_part (A,loc,val)),(SC_assignment ((denaming (V,A,(loc /. 4))),z)));