let V, A be set ; :: thesis: 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; :: thesis: for S being FinSequence st S IsNDRankSeq V,A & n in dom S holds
S | n IsNDRankSeq V,A
let S be FinSequence; :: thesis: ( S IsNDRankSeq V,A & n in dom S implies S | n IsNDRankSeq V,A )
assume A1: S IsNDRankSeq V,A ; :: thesis: ( not n in dom S or S | n IsNDRankSeq V,A )
assume A2: n in dom S ; :: thesis: 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; :: thesis: verum