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