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