let V, A be set ; :: thesis: for D being NonatomicND of V,A ex n being Nat st D is TypeSSNominativeData of V,(A \/ ((FNDSC (V,A)) . n))

let D be NonatomicND of V,A; :: thesis: ex n being Nat st D is TypeSSNominativeData of V,(A \/ ((FNDSC (V,A)) . n))

set F = FNDSC (V,A);

consider S being FinSequence such that

A1: S IsNDRankSeq V,A and

A2: D in Union S by Def5;

consider x being object such that

A3: x in dom S and

A4: D in S . x by A2, CARD_5:2;

reconsider x = x as Element of NAT by A3;

reconsider n = x - 1 as Element of NAT by A3, FINSEQ_3:25, INT_1:5;

take n ; :: thesis: D is TypeSSNominativeData of V,(A \/ ((FNDSC (V,A)) . n))

A5: (FNDSC (V,A)) . (n + 1) = S . (n + 1) by A1, A3, Th19;

(FNDSC (V,A)) . (n + 1) = NDSS (V,(A \/ ((FNDSC (V,A)) . n))) by Def3;

hence D is TypeSSNominativeData of V,(A \/ ((FNDSC (V,A)) . n)) by A4, A5, Th4; :: thesis: verum

let D be NonatomicND of V,A; :: thesis: ex n being Nat st D is TypeSSNominativeData of V,(A \/ ((FNDSC (V,A)) . n))

set F = FNDSC (V,A);

consider S being FinSequence such that

A1: S IsNDRankSeq V,A and

A2: D in Union S by Def5;

consider x being object such that

A3: x in dom S and

A4: D in S . x by A2, CARD_5:2;

reconsider x = x as Element of NAT by A3;

reconsider n = x - 1 as Element of NAT by A3, FINSEQ_3:25, INT_1:5;

take n ; :: thesis: D is TypeSSNominativeData of V,(A \/ ((FNDSC (V,A)) . n))

A5: (FNDSC (V,A)) . (n + 1) = S . (n + 1) by A1, A3, Th19;

(FNDSC (V,A)) . (n + 1) = NDSS (V,(A \/ ((FNDSC (V,A)) . n))) by Def3;

hence D is TypeSSNominativeData of V,(A \/ ((FNDSC (V,A)) . n)) by A4, A5, Th4; :: thesis: verum