set f = <*d1*>;
let n be Nat; :: according to NOMIN_7:def 6 :: thesis: ( 1 <= n & n <= len <*d1*> implies <*d1*> . n is NonatomicND of V,A )
assume A1: ( 1 <= n & n <= len <*d1*> ) ; :: thesis: <*d1*> . n is NonatomicND of V,A
len <*d1*> = 1 by FINSEQ_1:39;
then n = 1 by A1, XXREAL_0:1;
hence <*d1*> . n is NonatomicND of V,A ; :: thesis: verum