let V, A be set ; :: thesis: for S1, S2 being FinSequence st S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A holds
S1 tolerates S2
let S1, S2 be FinSequence; :: thesis: ( S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A implies S1 tolerates S2 )
assume that
A1: S1 IsNDRankSeq V,A and
A2: S2 IsNDRankSeq V,A ; :: thesis: S1 tolerates S2
let x be object ; :: according to PARTFUN1:def 4 :: thesis: ( not x in (dom S1) /\ (dom S2) or S1 . x = S2 . x )
assume A3: x in (dom S1) /\ (dom S2) ; :: thesis: S1 . x = S2 . x
defpred S₁[ Nat] means ( $1 in (dom S1) /\ (dom S2) implies S1 . $1 = S2 . $1 );
A4: S₁[ 0 ]

proof

assume 0 in (dom S1) /\ (dom S2) ; :: thesis: S1 . 0 = S2 . 0
then 0 in dom S1 by XBOOLE_0:def 4;
hence S1 . 0 = S2 . 0 by FINSEQ_3:24; :: thesis: verum

end;

A5: 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
A6: S₁[n] and
A7: n + 1 in (dom S1) /\ (dom S2) ; :: thesis: S1 . (n + 1) = S2 . (n + 1)
A8: n + 1 in dom S1 by A7, XBOOLE_0:def 4;
A9: n + 1 in dom S2 by A7, XBOOLE_0:def 4;

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

suppose n = 0 ; :: thesis: S1 . (n + 1) = S2 . (n + 1)

hence S1 . (n + 1) = S2 . (n + 1) by A1, A2; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: S1 . (n + 1) = S2 . (n + 1)

then A10: 1 <= n by NAT_1:14;
A11: n <= n + 1 by NAT_1:11;
n + 1 <= len S1 by A8, FINSEQ_3:25;
then n <= len S1 by A11, XXREAL_0:2;
then A12: n in dom S1 by A10, FINSEQ_3:25;
n + 1 <= len S2 by A9, FINSEQ_3:25;
then n <= len S2 by A11, XXREAL_0:2;
then n in dom S2 by A10, FINSEQ_3:25;
hence S2 . (n + 1) = NDSS (V,(A \/ (S1 . n))) by A2, A6, A9, A12, XBOOLE_0:def 4
.= S1 . (n + 1) by A1, A8, A12 ;
:: thesis: verum

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A5);
hence S1 . x = S2 . x by A3; :: thesis: verum