theorem :: NOMIN_1:12
for V, A being set
for n being Nat st 1 <= n holds
{} in (FNDSC (V,A)) . n