:: deftheorem defines valid_factorial_input_pred NOMIN_5:def 14 :
for V, A being set
for val being Function
for n0 being Nat
for d being object holds
( valid_factorial_input_pred V,A,val,n0,d iff ex d1 being NonatomicND of V,A st
( d = d1 & {(val . 1),(val . 2),(val . 3),(val . 4)} c= dom d1 & d1 . (val . 1) = 0 & d1 . (val . 2) = 1 & d1 . (val . 3) = n0 & d1 . (val . 4) = 1 ) );