dom <:((f . x) --> [f,x]),(id (f . x)):> = (dom ((f . x) --> [f,x])) /\ (dom (id (f . x))) by FUNCT_3:def 7
.= f . x ;
hence <:((f . x) --> [f,x]),(id (f . x)):> is ManySortedSet of f . x by PARTFUN1:def 2, RELAT_1:def 18; :: thesis: verum