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

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

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, Th1 ;

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;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, Th1 ;

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