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)

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;

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 Union (FNDSC (V,A)) or x in ND (V,A) )
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;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

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 )
;

end;

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;then x is TypeSCNominativeData of V,A by Def6;

hence x in ND (V,A) ; :: thesis: verum

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