per cases ( x in I or x nin dom R ) ;

suppose x in I ; :: thesis: R . x is Relation of (X . x),(Y . x)

hence R . x is Relation of (X . x),(Y . x) by MSUALG_4:def 1; :: thesis: verum

end;

suppose x nin dom R ; :: thesis: R . x is Relation of (X . x),(Y . x)

then R . x = {} by FUNCT_1:def 2;
hence R . x is Relation of (X . x),(Y . x) by XBOOLE_1:2; :: thesis: verum

end;

end;