:: deftheorem defines factorial_inv_pred NOMIN_5:def 18 :
for V, A being set
for loc being b₁ -valued Function
for n0 being Nat
for d being object holds
( factorial_inv_pred A,loc,n0,d iff ex d1 being NonatomicND of V,A st
( d = d1 & {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} c= dom d1 & d1 . (loc /. 2) = 1 & d1 . (loc /. 3) = n0 & ex I, S being Nat st
( I = d1 . (loc /. 1) & S = d1 . (loc /. 4) & S = I ! ) ) );