let V, A be set ; 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; 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; ( 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
; S . m c= S . n
per cases
( m <> 0 or m = 0 )
;
suppose A4:
m <> 0
;
S . m c= S . nthen 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;
verum end; end;