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

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 :: thesis: for i, j being Object of C holds M1 . (i,j) = M2 . (i,j)

hence
M1 = M2
by ALTCAT_1:7; :: thesis: verumlet 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;thus M1 . (i,j) = Hom (i,j) by A1

.= M2 . (i,j) by A2 ; :: thesis: verum