theorem Th18: :: NOMIN_9:18

for A being set
for x0, y0, p0, q0 being Integer
for n0 being Nat
for V being non empty set
for loc being b₇ -valued 10 -element FinSequence
for val being 10 -element FinSequence st A is complex-containing & A is_without_nonatomicND_wrt V & ( 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 ) ) & loc is one-to-one & loc,val are_different_wrt 10 holds
<*(valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)),(Lucas_main_part (A,loc,val)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))))*> is SFHT of (ND (V,A))