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 = (FNDSC (V,A)) . n

let n be Nat; :: thesis: for S being FinSequence st S IsNDRankSeq V,A & n in dom S holds

S . n = (FNDSC (V,A)) . n

let S be FinSequence; :: thesis: ( S IsNDRankSeq V,A & n in dom S implies S . n = (FNDSC (V,A)) . n )

assume A1: S IsNDRankSeq V,A ; :: thesis: ( not n in dom S or S . n = (FNDSC (V,A)) . n )

set F = FNDSC (V,A);

defpred S_{1}[ Nat] means ( $1 in dom S implies S . $1 = (FNDSC (V,A)) . $1 );

A2: S_{1}[ 0 ]
by FINSEQ_3:24;

A3: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A2, A3);

hence ( not n in dom S or S . n = (FNDSC (V,A)) . n ) ; :: thesis: verum

for S being FinSequence st S IsNDRankSeq V,A & n in dom S holds

S . n = (FNDSC (V,A)) . n

let n be Nat; :: thesis: for S being FinSequence st S IsNDRankSeq V,A & n in dom S holds

S . n = (FNDSC (V,A)) . n

let S be FinSequence; :: thesis: ( S IsNDRankSeq V,A & n in dom S implies S . n = (FNDSC (V,A)) . n )

assume A1: S IsNDRankSeq V,A ; :: thesis: ( not n in dom S or S . n = (FNDSC (V,A)) . n )

set F = FNDSC (V,A);

defpred S

A2: S

A3: for n being Nat st S

S

proof

for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume that

A4: S_{1}[n]
and

A5: n + 1 in dom S ; :: thesis: S . (n + 1) = (FNDSC (V,A)) . (n + 1)

end;assume that

A4: S

A5: n + 1 in dom S ; :: thesis: S . (n + 1) = (FNDSC (V,A)) . (n + 1)

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

end;

suppose
n <> 0
; :: thesis: S . (n + 1) = (FNDSC (V,A)) . (n + 1)

then A6:
1 <= n
by NAT_1:14;

A7: n + 1 <= len S by A5, FINSEQ_3:25;

n <= n + 1 by NAT_1:11;

then A8: n <= len S by A7, XXREAL_0:2;

then n in dom S by A6, FINSEQ_3:25;

hence S . (n + 1) = NDSS (V,(A \/ (S . n))) by A1, A5

.= (FNDSC (V,A)) . (n + 1) by A4, A6, A8, Def3, FINSEQ_3:25 ;

:: thesis: verum

end;A7: n + 1 <= len S by A5, FINSEQ_3:25;

n <= n + 1 by NAT_1:11;

then A8: n <= len S by A7, XXREAL_0:2;

then n in dom S by A6, FINSEQ_3:25;

hence S . (n + 1) = NDSS (V,(A \/ (S . n))) by A1, A5

.= (FNDSC (V,A)) . (n + 1) by A4, A6, A8, Def3, FINSEQ_3:25 ;

:: thesis: verum

hence ( not n in dom S or S . n = (FNDSC (V,A)) . n ) ; :: thesis: verum