A3: ND_ex_1 (v,D) = v .--> D ;

per cases ( D in A or D is NonatomicND of V,A ) by A1, Def6;

suppose D in A ; :: thesis: v .--> D is NonatomicND of V,A

hence v .--> D is NonatomicND of V,A by A2, A3, Th46; :: thesis: verum

end;

suppose D is NonatomicND of V,A ; :: thesis: v .--> D is NonatomicND of V,A

then consider F being FinSequence such that
A4: F IsNDRankSeq V,A and
A5: D in Union F by Def5;
consider Z being set such that
A6: D in Z and
A7: Z in rng F by A5, TARSKI:def 4;
reconsider Z = Z as non empty set by A6;
reconsider D1 = D as Element of Z by A6;
reconsider V = V as non empty set by A2;
reconsider v = v as Element of V by A2;
set d = v .--> D;
v .--> D1 is NominativeSet of V,Z ;
then A8: v .--> D in NDSS (V,Z) ;
A9: NDSS (V,Z) c= NDSS (V,(A \/ Z)) by Th7, XBOOLE_1:7;
consider x being object such that
A10: x in dom F and
A11: F . x = Z by A7, FUNCT_1:def 3;
reconsider x = x as Nat by A10;
A12: x <= len F by A10, FINSEQ_3:25;
consider S being FinSequence such that
A13: len S = 1 + (len F) and
A14: S IsNDRankSeq V,A and
A15: for n being Nat st n in dom S holds
S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n))) by A4, Th26;
1 <= x + 1 by NAT_1:11;
then A16: x + 1 in dom S by A13, A12, XREAL_1:6, FINSEQ_3:25;
then S . (x + 1) = NDSS (V,(A \/ ((<*A*> ^ F) . (x + 1)))) by A15
.= NDSS (V,(A \/ Z)) by A10, A11, FINSEQ_3:103 ;
then NDSS (V,(A \/ Z)) in rng S by A16, FUNCT_1:def 3;
then v .--> D in Union S by A8, A9, TARSKI:def 4;
hence v .--> D is NonatomicND of V,A by A14, Def5; :: thesis: verum

end;

end;