let seq1, seq2 be ManySortedSet of NAT ; :: thesis: ( 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)):] ; :: thesis: 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; :: thesis: ( S1[k] implies S1[k + 1] )
assume A9: S1[k] ; :: thesis: S1[k + 1]
thus seq1 . (k + 1) = [:(seq1 . k),(D . (k + 1)):] by A4
.= seq2 . (k + 1) by A6, A9 ; :: thesis: 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 ; :: thesis: verum