let V, A be set ; for S being FinSequence st S IsNDRankSeq V,A holds
S ^ <*(NDSS (V,(A \/ (S . (len S)))))*> IsNDRankSeq V,A
let S be FinSequence; ( S IsNDRankSeq V,A implies S ^ <*(NDSS (V,(A \/ (S . (len S)))))*> IsNDRankSeq V,A )
assume A1:
S IsNDRankSeq V,A
; S ^ <*(NDSS (V,(A \/ (S . (len S)))))*> IsNDRankSeq V,A
set S1 = S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>;
S <> {}
by A1;
then
rng S <> {}
;
then
1 in dom S
by FINSEQ_3:32;
hence
(S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) . 1 = NDSS (V,A)
by A1, FINSEQ_1:def 7; NOMIN_1:def 4 for n being Nat st n in dom (S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) & n + 1 in dom (S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) holds
(S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) . (n + 1) = NDSS (V,(A \/ ((S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) . n)))
let n be Nat; ( n in dom (S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) & n + 1 in dom (S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) implies (S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) . (n + 1) = NDSS (V,(A \/ ((S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) . n))) )
assume that
A2:
n in dom (S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>)
and
A3:
n + 1 in dom (S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>)
; (S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) . (n + 1) = NDSS (V,(A \/ ((S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) . n)))
len <*(NDSS (V,(A \/ (S . (len S)))))*> = 1
by FINSEQ_1:39;
then A4:
len (S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) = 1 + (len S)
by FINSEQ_1:22;
A5:
1 <= n
by A2, FINSEQ_3:25;
A6:
1 <= n + 1
by NAT_1:14;
A7:
n + 1 <= len (S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>)
by A3, FINSEQ_3:25;
then
(n + 1) - 1 <= (1 + (len S)) - 1
by A4, XREAL_1:9;
then A8:
n in dom S
by A5, FINSEQ_3:25;
then A9:
(S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) . n = S . n
by FINSEQ_1:def 7;