let V, A be set ; :: thesis: for m, n being Nat
for S being FinSequence st S IsNDRankSeq V,A & m <= n & n in dom S holds
S . m c= S . n
let m, n be Nat; :: thesis: for S being FinSequence st S IsNDRankSeq V,A & m <= n & n in dom S holds
S . m c= S . n
let S be FinSequence; :: thesis: ( S IsNDRankSeq V,A & m <= n & n in dom S implies S . m c= S . n )
assume that
A1: S IsNDRankSeq V,A and
A2: m <= n and
A3: n in dom S ; :: thesis: S . m c= S . n

per cases ( m <> 0 or m = 0 ) ;

suppose A4: m <> 0 ; :: thesis: S . m c= S . n

then A5: 0 + 1 <= m by NAT_1:13;
n <= len S by A3, FINSEQ_3:25;
then m <= len S by A2, XXREAL_0:2;
then ( S . m = (FNDSC (V,A)) . m & S . n = (FNDSC (V,A)) . n ) by A1, A3, A5, Th19, FINSEQ_3:25;
hence S . m c= S . n by A2, A4, Th13; :: thesis: verum

end;

suppose A6: m = 0 ; :: thesis: S . m c= S . n

not 0 in dom S by FINSEQ_3:24;
hence S . m c= S . n by A6, FUNCT_1:def 2; :: thesis: verum

end;

end;