let n be Nat; for V, A being set
for f being b1,b2 -NonatomicND-yielding FinSequence st n in dom f holds
f . n is NonatomicND of V,A
let V, A be set ; for f being V,A -NonatomicND-yielding FinSequence st n in dom f holds
f . n is NonatomicND of V,A
let f be V,A -NonatomicND-yielding FinSequence; ( n in dom f implies f . n is NonatomicND of V,A )
assume
n in dom f
; f . n is NonatomicND of V,A
then
( 1 <= n & n <= len f )
by FINSEQ_3:25;
hence
f . n is NonatomicND of V,A
by Def6; verum