assume A2:
not D . v in A
; NOMIN_1:def 6 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 A9:
z > 1
;
D . v is NonatomicND of V,Areconsider 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
;
D . v is Function
per cases
( lS = 1 or lS > 1 )
by A12, XXREAL_0:1;
suppose A18:
lS > 1
;
D . v is Functionthen 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
;
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;
verum end; end;