:: deftheorem defines valid_Lucas_output NOMIN_9:def 13 :
for V, A being set
for z being Element of V
for x0, y0, p0, q0 being Integer
for n0 being Nat holds valid_Lucas_output (A,z,x0,y0,p0,q0,n0) = valid_output (V,A,z,(Lucas (x0,y0,p0,q0,n0)));