:: deftheorem Def19 defines factorial_inv NOMIN_5:def 19 :
for V, A being set
for loc being b₁ -valued Function
for n0 being Nat
for b₅ being SCPartialNominativePredicate of V,A holds
( b₅ = factorial_inv (A,loc,n0) iff ( dom b₅ = ND (V,A) & ( for d being object st d in dom b₅ holds
( ( factorial_inv_pred A,loc,n0,d implies b₅ . d = TRUE ) & ( not factorial_inv_pred A,loc,n0,d implies b₅ . d = FALSE ) ) ) ) );