let n be Nat; :: thesis: for V, A being set
for f being b₁,b₂ -NonatomicND-yielding FinSequence st n in dom f holds
f . n is NonatomicND of V,A
let V, A be set ; :: thesis: 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; :: thesis: ( n in dom f implies f . n is NonatomicND of V,A )
assume n in dom f ; :: thesis: 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; :: thesis: verum