:: deftheorem defines power_main_part NOMIN_6:def 5 :
for V, A being set
for loc being b₁ -valued Function
for val being Function holds power_main_part (A,loc,val) = PP_composition ((power_var_init (A,loc,val)),(power_main_loop (A,loc)));