let A be set ; 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:]; ( ( 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)
; M = N
A2:
now for x being object st x in [:A,A,A:] holds
M . x = N . xlet x be
object ;
( x in [:A,A,A:] implies M . x = N . x )assume A3:
x in [:A,A,A:]
;
M . x = N . xthen 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
;
verum end;
( dom M = [:A,A,A:] & dom N = [:A,A,A:] )
by PARTFUN1:def 2;
hence
M = N
by A2, FUNCT_1:2; verum