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₁[ Nat] means ( $1 in dom S implies S . $1 = (FNDSC (V,A)) . $1 );
A2: S₁[ 0 ] by FINSEQ_3:24;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume that
A4: S₁[n] and
A5: n + 1 in dom S ; :: thesis: S . (n + 1) = (FNDSC (V,A)) . (n + 1)

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

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

hence S . (n + 1) = (FNDSC (V,A)) . (n + 1) by A1, Th9; :: thesis: verum

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;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence ( not n in dom S or S . n = (FNDSC (V,A)) . n ) ; :: thesis: verum