deffunc H_{1}( Object of C, Object of C) -> Element of bool the carrier' of C = Hom ($1,$2);

thus ex M being ManySortedSet of [: the carrier of C, the carrier of C:] st

for i, j being Object of C holds M . (i,j) = H_{1}(i,j)
from ALTCAT_1:sch 2(); :: thesis: verum

thus ex M being ManySortedSet of [: the carrier of C, the carrier of C:] st

for i, j being Object of C holds M . (i,j) = H