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;

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;

end;

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;hence D . v is NonatomicND of V,A by A1, A2, PARTFUN1:4; :: thesis: verum

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 )

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

(S | lS) . lS = S . lS
by FINSEQ_3:112;
assume A17:
not D . v in A
; :: thesis: D . v is Function

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

end;

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;then ex w being TypeSSNominativeData of V,A st w = D . v by A3;

hence D . v is Function ; :: thesis: verum

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

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