deffunc H₁( Object of , Object of ) -> Element of bool the U4 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 holds M . i,j = H₁(i,j) from ALTCAT_1:sch 2(); :: thesis: verum