per cases ( ( x in dom F & y in dom F ) or not x in dom F or not y in dom F ) ;

suppose ( x in dom F & y in dom F ) ; :: thesis: ( Swap F,x,y is Relation-like & Swap F,x,y is Function-like )

then Swap F,x,y = (F +* x,(F . y)) +* y,(F . x) by Def12;
hence ( Swap F,x,y is Relation-like & Swap F,x,y is Function-like ) ; :: thesis: verum

end;

suppose ( not x in dom F or not y in dom F ) ; :: thesis: ( Swap F,x,y is Relation-like & Swap F,x,y is Function-like )

hence ( Swap F,x,y is Relation-like & Swap F,x,y is Function-like ) by Def12; :: thesis: verum

end;

end;