let V, A be set ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 S_{1}[ Nat] means ( $1 + 1 in dom S implies S . ($1 + 1) = (FNDSC (V,A)) . ($1 + 1) );

A7: S_{1}[ 0 ]
by A2, A3, Def3;

A8: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A7, A8);

1 <= z by A5, FINSEQ_3:25;

( 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; :: thesis: ( 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 ; :: thesis: 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 S

A7: S

A8: for n being Nat st S

S

proof

A13:
for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume that

A9: S_{1}[n]
and

A10: (n + 1) + 1 in dom S ; :: thesis: 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 ;

:: thesis: verum

end;assume that

A9: S

A10: (n + 1) + 1 in dom S ; :: thesis: 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 ;

:: thesis: verum

1 <= z by A5, FINSEQ_3:25;

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

end;

suppose A14:
z = 1
; :: thesis: 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; :: thesis: verum

end;(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; :: thesis: verum

suppose A16:
1 < z
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum