let R be ManySortedRelation of A,B; :: thesis: R is Relation-yielding
let x be set ; :: according to MSUALG_4:def 1 :: thesis: ( x in dom R implies R . x is Relation )
assume x in dom R ; :: thesis: R . x is Relation
then x in I by PARTFUN1:def 4;
hence R . x is Relation by Def2; :: thesis: verum