theorem Th15: :: NOMIN_9:15

for V, A being set
for loc being b₁ -valued Function
for d1 being NonatomicND of V,A st not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & d1 in dom (Lucas_loop_body (A,loc)) & loc is_valid_wrt d1 & Seg 10 c= dom loc & ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 2 is_a_value_on T & loc /. 4 is_a_value_on T & loc /. 6 is_a_value_on T & loc /. 7 is_a_value_on T & loc /. 8 is_a_value_on T & loc /. 9 is_a_value_on T & loc /. 10 is_a_value_on T ) ) holds
prg_doms_of loc,d1,<*(denaming (V,A,(loc /. 4))),(denaming (V,A,(loc /. 5))),(multiplication (A,(loc /. 7),(loc /. 4))),(multiplication (A,(loc /. 8),(loc /. 6))),(subtraction (A,(loc /. 9),(loc /. 10))),(addition (A,(loc /. 1),(loc /. 2)))*>,<*6,4,9,10,5,1*>