deffunc H₁( 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₁(i,j) from ALTCAT_1:sch 2(); :: thesis: verum