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;