let R be ManySortedRelation of A,B; :: thesis: R is Relation-yielding
let x be set ; :: according to FUNCOP_1:def 11 :: thesis: ( not x in proj1 R or R . x is set )
assume x in dom R ; :: thesis: R . x is set
then x in I by PARTFUN1:def 2;
hence R . x is set by Def2; :: thesis: verum