thus ( f is V,A -NonatomicND-yielding implies for n being Nat st 1 <= n & n <= len f holds
f . n is NonatomicND of V,A ) by FINSEQ_3:25; :: thesis: ( ( for n being Nat st 1 <= n & n <= len f holds
f . n is NonatomicND of V,A ) implies f is V,A -NonatomicND-yielding )
assume A1: for n being Nat st 1 <= n & n <= len f holds
f . n is NonatomicND of V,A ; :: thesis: f is V,A -NonatomicND-yielding
let n be object ; :: according to NOMIN_7:def 5 :: thesis: ( n in dom f implies f . n is NonatomicND of V,A )
assume A2: n in dom f ; :: thesis: f . n is NonatomicND of V,A
reconsider n = n as Element of NAT by A2;
( 1 <= n & n <= len f ) by A2, FINSEQ_3:25;
hence f . n is NonatomicND of V,A by A1; :: thesis: verum