let seq1, seq2 be ManySortedSet of NAT ; ( seq1 . 0 = D . 0 & ( for i being Nat holds seq1 . (i + 1) = [:(seq1 . i),(D . (i + 1)):] ) & seq2 . 0 = D . 0 & ( for i being Nat holds seq2 . (i + 1) = [:(seq2 . i),(D . (i + 1)):] ) implies seq1 = seq2 )
assume that
A3:
seq1 . 0 = D . 0
and
A4:
for i being Nat holds seq1 . (i + 1) = [:(seq1 . i),(D . (i + 1)):]
and
A5:
seq2 . 0 = D . 0
and
A6:
for i being Nat holds seq2 . (i + 1) = [:(seq2 . i),(D . (i + 1)):]
; seq1 = seq2
A7:
dom seq2 = NAT
by PARTFUN1:def 2;
defpred S1[ Nat] means seq1 . $1 = seq2 . $1;
A8:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A9:
S1[
k]
;
S1[k + 1]
thus seq1 . (k + 1) =
[:(seq1 . k),(D . (k + 1)):]
by A4
.=
seq2 . (k + 1)
by A6, A9
;
verum
end;
A10:
S1[ 0 ]
by A3, A5;
A11:
for n being Nat holds S1[n]
from NAT_1:sch 2(A10, A8);
for n being object st n in dom seq1 holds
seq1 . n = seq2 . n
by A11;
hence
seq1 = seq2
by A7, FUNCT_1:2, PARTFUN1:def 2; verum