theorem Th13: :: NOMIN_9:13

for V, A being set
for loc being b₁ -valued Function
for x0, y0, p0, q0 being Integer
for n0 being Nat
for val being 10 -element FinSequence st not V is empty & A is_without_nonatomicND_wrt V & Seg 10 c= dom loc & loc | (Seg 10) is one-to-one & loc,val are_different_wrt 10 holds
valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0) ||= (SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . (len (SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))))