let F be Function; :: thesis: for x, y being set holds dom (Swap F,x,y) = dom F
let x, y be set ; :: 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 Def12
.= dom (F +* x,(F . y)) by Th32
.= dom F by Th32 ;
:: 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 Def12; :: thesis: verum

end;

end;