let V, A be set ; :: thesis: ND (V,A) = Union (FNDSC (V,A))
set F = FNDSC (V,A);
thus ND (V,A) c= Union (FNDSC (V,A)) :: according to XBOOLE_0:def 10 :: thesis: Union (FNDSC (V,A)) c= ND (V,A)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ND (V,A) or x in Union (FNDSC (V,A)) )
assume x in ND (V,A) ; :: thesis: x in Union (FNDSC (V,A))
then x is TypeSCNominativeData of V,A by Th39;
then A1: ( x in A or x is NonatomicND of V,A ) by Def6;
A c= Union (FNDSC (V,A)) by Th11;
hence x in Union (FNDSC (V,A)) by A1, Th31; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union (FNDSC (V,A)) or x in ND (V,A) )
assume x in Union (FNDSC (V,A)) ; :: thesis: x in ND (V,A)
then consider z being object such that
A2: z in dom (FNDSC (V,A)) and
A3: x in (FNDSC (V,A)) . z by CARD_5:2;
reconsider z = z as Element of NAT by A2, Def3;

per cases ( z = 0 or z <> 0 ) ;

suppose z = 0 ; :: thesis: x in ND (V,A)

then x in A by A3, Def3;
then x is TypeSCNominativeData of V,A by Def6;
hence x in ND (V,A) ; :: thesis: verum

end;

suppose A4: z <> 0 ; :: thesis: x in ND (V,A)

then A5: 1 <= z by NAT_1:14;
reconsider n = z - 1 as Element of NAT by A4, INT_1:5, NAT_1:14;
A6: dom (FNDSC (V,A)) = NAT by Def3;
set S = (FNDSC (V,A)) | (Seg z);
(FNDSC (V,A)) . (n + 1) = NDSS (V,(A \/ ((FNDSC (V,A)) . n))) by Def3;
then A7: x is TypeSSNominativeData of V,(A \/ ((FNDSC (V,A)) . n)) by A3, Th4;
A8: dom ((FNDSC (V,A)) | (Seg z)) = Seg z by A6, RELAT_1:62;
A9: z in Seg z by A5;
then ((FNDSC (V,A)) | (Seg z)) . z = (FNDSC (V,A)) . z by FUNCT_1:49;
then (FNDSC (V,A)) . z in rng ((FNDSC (V,A)) | (Seg z)) by A8, A9, FUNCT_1:def 3;
then x in Union ((FNDSC (V,A)) | (Seg z)) by A3, TARSKI:def 4;
then x is NonatomicND of V,A by A7, A5, Th18, Def5;
hence x in ND (V,A) ; :: thesis: verum

end;

end;