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 Def11;
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 Def11; :: thesis: verum

end;

end;