let M1, M2 be ManySortedSet of [:the carrier of C,the carrier of C:]; :: thesis: ( ( for i, j being Object of C holds M1 . i,j = Hom i,j ) & ( for i, j being Object of C holds M2 . i,j = Hom i,j ) implies M1 = M2 )
assume that
A1: for i, j being Object of C holds M1 . i,j = Hom i,j and
A2: for i, j being Object of C holds M2 . i,j = Hom i,j ; :: thesis: M1 = M2

now

let i, j be Object of C; :: thesis: M1 . i,j = M2 . i,j
thus M1 . i,j = Hom i,j by A1
.= M2 . i,j by A2 ; :: thesis: verum

end;

hence M1 = M2 by ALTCAT_1:9; :: thesis: verum