let V, A be set ; for f being Function st ex S being FinSequence st
( S IsNDRankSeq V,A & f in Union S ) holds
f in Union (FNDSC (V,A))
set F = FNDSC (V,A);
A1:
dom (FNDSC (V,A)) = NAT
by Def3;
A2:
(FNDSC (V,A)) . 0 = A \/ A
by Def3;
let f be Function; ( ex S being FinSequence st
( S IsNDRankSeq V,A & f in Union S ) implies f in Union (FNDSC (V,A)) )
given S being FinSequence such that A3:
S IsNDRankSeq V,A
and
A4:
f in Union S
; f in Union (FNDSC (V,A))
consider z being object such that
A5:
z in dom S
and
A6:
f in S . z
by A4, CARD_5:2;
reconsider z = z as Element of NAT by A5;
defpred S1[ Nat] means ( $1 + 1 in dom S implies S . ($1 + 1) = (FNDSC (V,A)) . ($1 + 1) );
A7:
S1[ 0 ]
by A2, A3, Def3;
A8:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume that A9:
S1[
n]
and A10:
(n + 1) + 1
in dom S
;
S . ((n + 1) + 1) = (FNDSC (V,A)) . ((n + 1) + 1)
A11:
(n + 1) + 1
<= len S
by A10, FINSEQ_3:25;
n + 1
<= (n + 1) + 1
by NAT_1:11;
then A12:
n + 1
<= len S
by A11, XXREAL_0:2;
then
n + 1
in dom S
by NAT_1:11, FINSEQ_3:25;
hence S . ((n + 1) + 1) =
NDSS (
V,
(A \/ (S . (n + 1))))
by A3, A10
.=
(FNDSC (V,A)) . ((n + 1) + 1)
by A9, A12, Def3, NAT_1:11, FINSEQ_3:25
;
verum
end;
A13:
for n being Nat holds S1[n]
from NAT_1:sch 2(A7, A8);
1 <= z
by A5, FINSEQ_3:25;
per cases then
( z = 1 or 1 < z )
by XXREAL_0:1;
suppose A14:
z = 1
;
f in Union (FNDSC (V,A))A15:
(FNDSC (V,A)) . (0 + 1) = NDSS (
V,
(A \/ ((FNDSC (V,A)) . 0)))
by Def3;
(FNDSC (V,A)) . 1
in rng (FNDSC (V,A))
by A1, FUNCT_1:def 3;
hence
f in Union (FNDSC (V,A))
by A2, A3, A6, A14, A15, TARSKI:def 4;
verum end; suppose A16:
1
< z
;
f in Union (FNDSC (V,A))then reconsider lZ =
z - 1 as
Element of
NAT by INT_1:5;
1
- 1
< lZ
by A16, XREAL_1:14;
then
0 + 1
<= lZ
by NAT_1:13;
then reconsider r =
lZ - 1 as
Element of
NAT by INT_1:5;
A17:
S . (lZ + 1) = NDSS (
V,
(A \/ (S . lZ)))
by A3, A5, A16, CGAMES_1:20;
A18:
(FNDSC (V,A)) . (r + 1) = S . (r + 1)
by A5, A13, A16, CGAMES_1:20;
(FNDSC (V,A)) . (lZ + 1) = NDSS (
V,
(A \/ ((FNDSC (V,A)) . lZ)))
by Def3;
then
NDSS (
V,
(A \/ (S . lZ)))
in rng (FNDSC (V,A))
by A1, A18, FUNCT_1:def 3;
hence
f in Union (FNDSC (V,A))
by A6, A17, TARSKI:def 4;
verum end;