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

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 )
;

end;

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;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