let V, A be set ; for n being Nat
for S being FinSequence st S IsNDRankSeq V,A & n in dom S holds
S | n IsNDRankSeq V,A
let n be Nat; for S being FinSequence st S IsNDRankSeq V,A & n in dom S holds
S | n IsNDRankSeq V,A
let S be FinSequence; ( S IsNDRankSeq V,A & n in dom S implies S | n IsNDRankSeq V,A )
assume A1:
S IsNDRankSeq V,A
; ( not n in dom S or S | n IsNDRankSeq V,A )
assume A2:
n in dom S
; S | n IsNDRankSeq V,A
then
n <= len S
by FINSEQ_3:25;
then
len (S | n) = n
by FINSEQ_1:17;
then
S | n <> {}
by A2, FINSEQ_3:24;
hence
S | n IsNDRankSeq V,A
by A1, RELAT_1:59, Th15; verum