theorem Th58: :: NOMIN_1:58

for a being object
for V, A being set
for n being Nat
for f being b₂ -valued FinSequence st 1 <= n & n <= len f holds
(namingSeq (V,A,f,a)) . n is NonatomicND of V,A