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 S_{1}[ Nat] means seq1 . $1 = seq2 . $1;

A8: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by A3, A5;

A11: for n being Nat holds S_{1}[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; :: thesis: verum

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 S

A8: for k being Nat st S

S

proof

A10:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A9: S_{1}[k]
; :: thesis: S_{1}[k + 1]

thus seq1 . (k + 1) = [:(seq1 . k),(D . (k + 1)):] by A4

.= seq2 . (k + 1) by A6, A9 ; :: thesis: verum

end;assume A9: S

thus seq1 . (k + 1) = [:(seq1 . k),(D . (k + 1)):] by A4

.= seq2 . (k + 1) by A6, A9 ; :: thesis: verum

A11: for n being Nat holds S

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; :: thesis: verum