let M1, M2 be ManySortedSet of [:I,I,I:]; :: thesis: ( ( for i, j, k being object 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 object 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
A6: for i, j, k being object st i in I & j in I & k in I holds
M1 . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] and
A7: for i, j, k being object 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 :: thesis: 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 ; :: thesis: ( i in I & j in I & k in I implies M1 . (i,j,k) = M2 . (i,j,k) )
assume A8: ( 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 A6
.= M2 . (i,j,k) by A7, A8 ;
:: thesis: verum

end;

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