:: deftheorem Def15 defines Lucas_inv NOMIN_9:def 15 :
for V, A being set
for loc being b₁ -valued Function
for x0, y0, p0, q0 being Integer
for n0 being Nat
for b₉ being SCPartialNominativePredicate of V,A holds
( b₉ = Lucas_inv (A,loc,x0,y0,p0,q0,n0) iff ( dom b₉ = ND (V,A) & ( for d being object st d in dom b₉ holds
( ( Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d implies b₉ . d = TRUE ) & ( not Lucas_inv_pred A,loc,x0,y0,p0,q0,n0,d implies b₉ . d = FALSE ) ) ) ) );