assume A2: not D . v in A ; :: according to NOMIN_1:def 6 :: thesis: D . v is NonatomicND of V,A
consider S being FinSequence such that
A3: S IsNDRankSeq V,A and
A4: D in Union S by Def5;
consider Z being set such that
A5: D in Z and
A6: Z in rng S by A4, TARSKI:def 4;
consider z being object such that
A7: z in dom S and
A8: S . z = Z by A6, FUNCT_1:def 3;
reconsider z = z as Element of NAT by A7;
1 <= z by A7, FINSEQ_3:25;

per cases then ( z = 1 or z > 1 ) by XXREAL_0:1;

suppose z = 1 ; :: thesis: D . v is NonatomicND of V,A

then ex w being TypeSSNominativeData of V,A st w = D by A3, A5, A8;
hence D . v is NonatomicND of V,A by A1, A2, PARTFUN1:4; :: thesis: verum

end;

suppose A9: z > 1 ; :: thesis: D . v is NonatomicND of V,A

reconsider lS = z - 1 as Element of NAT by A7, FINSEQ_3:25, INT_1:5;
set S1 = S | lS;
A10: dom (S | lS) c= dom S by RELAT_1:60;
A11: z <= len S by A7, FINSEQ_3:25;
1 - 1 < lS by A9, XREAL_1:14;
then A12: 0 + 1 <= lS by NAT_1:13;
lS <= z - 0 by XREAL_1:10;
then len (S | lS) = lS by A11, XXREAL_0:2, FINSEQ_1:59;
then A13: lS in dom (S | lS) by A12, FINSEQ_3:25;
then S . (lS + 1) = NDSS (V,(A \/ (S . lS))) by A7, A3, A10;
then consider d being TypeSSNominativeData of V,(A \/ (S . lS)) such that
A14: D = d by A5, A8;
A15: D . v in A \/ (S . lS) by A1, A14, PARTFUN1:4;
A16: ( not D . v in A implies D . v is Function )

proof

assume A17: not D . v in A ; :: thesis: D . v is Function

per cases ( lS = 1 or lS > 1 ) by A12, XXREAL_0:1;

suppose lS = 1 ; :: thesis: D . v is Function

then D . v in S . 1 by A15, A17, XBOOLE_0:def 3;
then ex w being TypeSSNominativeData of V,A st w = D . v by A3;
hence D . v is Function ; :: thesis: verum

end;

suppose A18: lS > 1 ; :: thesis: D . v is Function

then reconsider c = lS - 1 as Element of NAT by INT_1:5;
c > 1 - 1 by A18, XREAL_1:14;
then A19: 1 <= c by NAT_1:14;
A20: lS <= len S by A10, A13, FINSEQ_3:25;
c <= lS - 0 by XREAL_1:10;
then c <= len S by A20, XXREAL_0:2;
then c in dom S by A19, FINSEQ_3:25;
then ( S . (c + 1) = NDSS (V,(A \/ (S . c))) & D . v in S . lS ) by A3, A10, A13, A15, A17, XBOOLE_0:def 3;
then ex w being TypeSSNominativeData of V,(A \/ (S . c)) st w = D . v ;
hence D . v is Function ; :: thesis: verum

end;

end;

end;

(S | lS) . lS = S . lS by FINSEQ_3:112;
then ( S . lS in rng (S | lS) & D . v in S . lS ) by A2, A13, A15, FUNCT_1:def 3, XBOOLE_0:def 3;
then D . v in Union (S | lS) by TARSKI:def 4;
hence D . v is NonatomicND of V,A by A2, A3, A10, A13, A16, Th16, Def5; :: thesis: verum

end;

end;