let M1, M2 be ManySortedSet of [: the carrier of C, the carrier of C:]; ( ( 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)
; M1 = M2
now for i, j being Object of C holds M1 . (i,j) = M2 . (i,j)let i,
j be
Object of
C;
M1 . (i,j) = M2 . (i,j)thus M1 . (
i,
j) =
Hom (
i,
j)
by A1
.=
M2 . (
i,
j)
by A2
;
verum end;
hence
M1 = M2
by ALTCAT_1:7; verum