let V, A be set ; :: thesis: for S being FinSequence st S IsNDRankSeq V,A holds
S ^ <*(NDSS (V,(A \/ (S . (len S)))))*> IsNDRankSeq V,A
let S be FinSequence; :: thesis: ( S IsNDRankSeq V,A implies S ^ <*(NDSS (V,(A \/ (S . (len S)))))*> IsNDRankSeq V,A )
assume A1: S IsNDRankSeq V,A ; :: thesis: 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; :: according to NOMIN_1:def 4 :: thesis: 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; :: thesis: ( 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)))))*>) ; :: thesis: (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;

per cases ( n + 1 < len (S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) or n + 1 = len (S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) ) by A7, XXREAL_0:1;

suppose n + 1 < len (S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) ; :: thesis: (S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) . (n + 1) = NDSS (V,(A \/ ((S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) . n)))

then n + 1 <= len S by A4, NAT_1:13;
then A10: n + 1 in dom S by A6, FINSEQ_3:25;
then (S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) . (n + 1) = S . (n + 1) by FINSEQ_1:def 7;
hence (S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) . (n + 1) = NDSS (V,(A \/ ((S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) . n))) by A1, A8, A9, A10; :: thesis: verum

end;

suppose n + 1 = len (S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) ; :: thesis: (S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) . (n + 1) = NDSS (V,(A \/ ((S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) . n)))

hence (S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) . (n + 1) = NDSS (V,(A \/ ((S ^ <*(NDSS (V,(A \/ (S . (len S)))))*>) . n))) by A4, A9, FINSEQ_1:42; :: thesis: verum

end;

end;