let V, A be set ; for F being FinSequence st F IsNDRankSeq V,A holds
ex S being FinSequence st
( len S = 1 + (len F) & S IsNDRankSeq V,A & ( for n being Nat st n in dom S holds
S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n))) ) )
let F be FinSequence; ( F IsNDRankSeq V,A implies ex S being FinSequence st
( len S = 1 + (len F) & S IsNDRankSeq V,A & ( for n being Nat st n in dom S holds
S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n))) ) ) )
assume A1:
F IsNDRankSeq V,A
; ex S being FinSequence st
( len S = 1 + (len F) & S IsNDRankSeq V,A & ( for n being Nat st n in dom S holds
S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n))) ) )
set G = <*A*> ^ F;
deffunc H1( object ) -> set = NDSS (V,(A \/ ((<*A*> ^ F) . $1)));
consider S being FinSequence such that
A2:
len S = len (<*A*> ^ F)
and
A3:
for n being Nat st n in dom S holds
S . n = H1(n)
from FINSEQ_1:sch 2();
take
S
; ( len S = 1 + (len F) & S IsNDRankSeq V,A & ( for n being Nat st n in dom S holds
S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n))) ) )
len <*A*> = 1
by FINSEQ_1:39;
hence A4:
len S = 1 + (len F)
by A2, FINSEQ_1:22; ( S IsNDRankSeq V,A & ( for n being Nat st n in dom S holds
S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n))) ) )
A5:
(<*A*> ^ F) . 1 = A
by FINSEQ_1:41;
A6:
for n being Nat st n in dom F holds
(<*A*> ^ F) . (n + 1) = F . n
by Th1;
A7:
1 <= len S
by A4, NAT_1:11;
thus
S IsNDRankSeq V,A
for n being Nat st n in dom S holds
S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n)))proof
thus A8:
S . 1 =
NDSS (
V,
(A \/ ((<*A*> ^ F) . 1)))
by A3, A7, FINSEQ_3:25
.=
NDSS (
V,
A)
by A5
;
NOMIN_1:def 4 for n being Nat st n in dom S & n + 1 in dom S holds
S . (n + 1) = NDSS (V,(A \/ (S . n)))
let n be
Nat;
( n in dom S & n + 1 in dom S implies S . (n + 1) = NDSS (V,(A \/ (S . n))) )
assume that A9:
n in dom S
and A10:
n + 1
in dom S
;
S . (n + 1) = NDSS (V,(A \/ (S . n)))
A11:
1
<= n
by A9, FINSEQ_3:25;
A12:
n <= len F
by A4, A10, FINSEQ_3:25, XREAL_1:6;
then A13:
n in dom F
by A11, FINSEQ_3:25;
per cases
( n = 1 or n > 1 )
by A11, XXREAL_0:1;
suppose A14:
n > 1
;
S . (n + 1) = NDSS (V,(A \/ (S . n)))then reconsider m =
n - 1 as
Element of
NAT by INT_1:5;
S . n =
NDSS (
V,
(A \/ ((<*A*> ^ F) . (m + 1))))
by A3, A9
.=
NDSS (
V,
(A \/ (F . m)))
by A13, A14, Th1, CGAMES_1:20
.=
F . (m + 1)
by A1, A13, A14, CGAMES_1:20
;
then
(<*A*> ^ F) . (n + 1) = S . n
by A6, A12, A11, FINSEQ_3:25;
hence
NDSS (
V,
(A \/ (S . n)))
= S . (n + 1)
by A3, A10;
verum end; end;
end;
thus
for n being Nat st n in dom S holds
S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n)))
by A3; verum