let A be set ; :: thesis: for N, M being ManySortedSet of [:A,A,A:] st ( for i, j, k being object st i in A & j in A & k in A holds

N . (i,j,k) = M . (i,j,k) ) holds

M = N

let N, M be ManySortedSet of [:A,A,A:]; :: thesis: ( ( for i, j, k being object st i in A & j in A & k in A holds

N . (i,j,k) = M . (i,j,k) ) implies M = N )

assume A1: for i, j, k being object st i in A & j in A & k in A holds

N . (i,j,k) = M . (i,j,k) ; :: thesis: M = N

hence M = N by A2, FUNCT_1:2; :: thesis: verum

N . (i,j,k) = M . (i,j,k) ) holds

M = N

let N, M be ManySortedSet of [:A,A,A:]; :: thesis: ( ( for i, j, k being object st i in A & j in A & k in A holds

N . (i,j,k) = M . (i,j,k) ) implies M = N )

assume A1: for i, j, k being object st i in A & j in A & k in A holds

N . (i,j,k) = M . (i,j,k) ; :: thesis: M = N

A2: now :: thesis: for x being object st x in [:A,A,A:] holds

M . x = N . x

( dom M = [:A,A,A:] & dom N = [:A,A,A:] )
by PARTFUN1:def 2;M . x = N . x

let x be object ; :: thesis: ( x in [:A,A,A:] implies M . x = N . x )

assume A3: x in [:A,A,A:] ; :: thesis: M . x = N . x

then reconsider A = A as non empty set by MCART_1:31;

consider i, j, k being Element of A such that

A4: x = [i,j,k] by A3, DOMAIN_1:3;

thus M . x = M . (i,j,k) by A4, MULTOP_1:def 1

.= N . (i,j,k) by A1

.= N . x by A4, MULTOP_1:def 1 ; :: thesis: verum

end;assume A3: x in [:A,A,A:] ; :: thesis: M . x = N . x

then reconsider A = A as non empty set by MCART_1:31;

consider i, j, k being Element of A such that

A4: x = [i,j,k] by A3, DOMAIN_1:3;

thus M . x = M . (i,j,k) by A4, MULTOP_1:def 1

.= N . (i,j,k) by A1

.= N . x by A4, MULTOP_1:def 1 ; :: thesis: verum

hence M = N by A2, FUNCT_1:2; :: thesis: verum