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_{1}[ Nat] means ( $1 in (dom S1) /\ (dom S2) implies S1 . $1 = S2 . $1 );

A4: S_{1}[ 0 ]
_{1}[n] holds

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

hence S1 . x = S2 . x by A3; :: thesis: verum

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

A4: S

proof

A5:
for n being Nat st S
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;then 0 in dom S1 by XBOOLE_0:def 4;

hence S1 . 0 = S2 . 0 by FINSEQ_3:24; :: thesis: verum

S

proof

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

assume that

A6: S_{1}[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;

end;assume that

A6: S

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

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

hence S1 . x = S2 . x by A3; :: thesis: verum