let M1, M2 be ManySortedSet of [:I,I,I:]; :: thesis: ( ( for i, j, k being set st i in I & j in I & k in I holds
M1 . i,j,k = [:(H . j,k),(G . i,j):] ) & ( for i, j, k being set st i in I & j in I & k in I holds
M2 . i,j,k = [:(H . j,k),(G . i,j):] ) implies M1 = M2 )
assume that
A4: for i, j, k being set st i in I & j in I & k in I holds
M1 . i,j,k = [:(H . j,k),(G . i,j):] and
A5: for i, j, k being set st i in I & j in I & k in I holds
M2 . i,j,k = [:(H . j,k),(G . i,j):] ; :: thesis: M1 = M2

now

let i, j, k be set ; :: thesis: ( i in I & j in I & k in I implies M1 . i,j,k = M2 . i,j,k )
assume A6: ( i in I & j in I & k in I ) ; :: thesis: M1 . i,j,k = M2 . i,j,k
hence M1 . i,j,k = [:(H . j,k),(G . i,j):] by A4
.= M2 . i,j,k by A5, A6 ;
:: thesis: verum

end;

hence M1 = M2 by Th10; :: thesis: verum