:: deftheorem Def11 defines Swap FUNCT_7:def 12 :
for F being Function
for x, y being object holds
( ( x in dom F & y in dom F implies Swap (F,x,y) = (F +* (x,(F . y))) +* (y,(F . x)) ) & ( ( not x in dom F or not y in dom F ) implies Swap (F,x,y) = F ) );