let V, A be set ; 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; 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
; 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; verum