theorem Th21: :: NOMIN_9:21

for V, A being set
for loc being b₁ -valued Function
for z being Element of V
for x0, y0, p0, q0 being Integer
for n0 being Nat st ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) holds
<*(PP_inversion (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))))),(SC_assignment ((denaming (V,A,(loc /. 4))),z)),(valid_Lucas_output (A,z,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A))