let F be Function; :: thesis: for x, y being object holds dom (Swap (F,x,y)) = dom F
let x, y be object ; :: thesis: dom (Swap (F,x,y)) = dom F

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: dom (Swap (F,x,y)) = dom F

hence dom (Swap (F,x,y)) = dom ((F +* (x,(F . y))) +* (y,(F . x))) by Def11
.= dom (F +* (x,(F . y))) by Th29
.= dom F by Th29 ;
:: thesis: verum

end;

suppose ( not x in dom F or not y in dom F ) ; :: thesis: dom (Swap (F,x,y)) = dom F

hence dom (Swap (F,x,y)) = dom F by Def11; :: thesis: verum

end;

end;