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