let M1, M2 be ManySortedSet of [:I,I,I:]; ( ( for i, j, k being object st i in I & j in I & k in I holds
M1 . (i,j,k) = G . (i,k) ) & ( for i, j, k being object st i in I & j in I & k in I holds
M2 . (i,j,k) = G . (i,k) ) implies M1 = M2 )
assume that
A2:
for i, j, k being object st i in I & j in I & k in I holds
M1 . (i,j,k) = G . (i,k)
and
A3:
for i, j, k being object st i in I & j in I & k in I holds
M2 . (i,j,k) = G . (i,k)
; M1 = M2
now for i, j, k being object st i in I & j in I & k in I holds
M1 . (i,j,k) = M2 . (i,j,k)let i,
j,
k be
object ;
( i in I & j in I & k in I implies M1 . (i,j,k) = M2 . (i,j,k) )assume A4:
(
i in I &
j in I &
k in I )
;
M1 . (i,j,k) = M2 . (i,j,k)hence M1 . (
i,
j,
k) =
G . (
i,
k)
by A2
.=
M2 . (
i,
j,
k)
by A3, A4
;
verum end;
hence
M1 = M2
by Th4; verum