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

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

suppose that A1: x in dom F and
A2: y in dom F ; :: thesis: rng (Swap (F,x,y)) = rng F

F . x in rng F by A1, FUNCT_1:3;
then F . x in (rng F) \/ {(F . y)} by XBOOLE_0:def 3;
then ((rng F) \/ {(F . y)}) \/ {(F . x)} = (rng F) \/ {(F . y)} by ZFMISC_1:40
.= rng F by A2, FUNCT_1:3, ZFMISC_1:40 ;
then A3: (rng (F +* (x,(F . y)))) \/ {(F . x)} c= rng F by Th102, XBOOLE_1:9;
A4: (F +* (x,(F . y))) . y = F . y

proof

per cases ( x <> y or x = y ) ;

suppose x <> y ; :: thesis: (F +* (x,(F . y))) . y = F . y

hence (F +* (x,(F . y))) . y = F . y by Th34; :: thesis: verum

end;

suppose x = y ; :: thesis: (F +* (x,(F . y))) . y = F . y

hence (F +* (x,(F . y))) . y = F . y by A1, Th33; :: thesis: verum

end;

end;

end;

A5: rng F c= (rng (F +* (x,(F . y)))) \/ {(F . x)} by Th103;
A6: Swap (F,x,y) = (F +* (x,(F . y))) +* (y,(F . x)) by A1, A2, Def12;
then rng (Swap (F,x,y)) c= (rng (F +* (x,(F . y)))) \/ {(F . x)} by Th102;
then A7: rng (Swap (F,x,y)) c= rng F by A3, XBOOLE_1:1;
A8: y in dom (F +* (x,(F . y))) by A2, Th32;
A9: F . y in rng (Swap (F,x,y))

proof

per cases ( F . x = F . y or F . x <> F . y ) ;

suppose F . x = F . y ; :: thesis: F . y in rng (Swap (F,x,y))

hence F . y in rng (Swap (F,x,y)) by A6, A8, Th104; :: thesis: verum

end;

suppose A10: F . x <> F . y ; :: thesis: F . y in rng (Swap (F,x,y))

A11: dom (Swap (F,x,y)) = dom F by Th101;
(Swap (F,x,y)) . x = (F +* (x,(F . y))) . x by A6, A10, Th34
.= F . y by A1, Th33 ;
hence F . y in rng (Swap (F,x,y)) by A1, A11, FUNCT_1:3; :: thesis: verum

end;

end;

end;

F . x in rng (Swap (F,x,y)) by A6, A8, Th104;
then F . x in (rng (Swap (F,x,y))) \/ {(F . y)} by XBOOLE_0:def 3;
then ((rng (Swap (F,x,y))) \/ {(F . y)}) \/ {(F . x)} = (rng (Swap (F,x,y))) \/ {(F . y)} by ZFMISC_1:40
.= rng (Swap (F,x,y)) by A9, ZFMISC_1:40 ;
then (rng (F +* (x,(F . y)))) \/ {(F . x)} c= rng (Swap (F,x,y)) by A6, A4, Th103, XBOOLE_1:9;
then rng F c= rng (Swap (F,x,y)) by A5, XBOOLE_1:1;
hence rng (Swap (F,x,y)) = rng F by A7, XBOOLE_0:def 10; :: thesis: verum

end;

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

hence rng (Swap (F,x,y)) = rng F by Def12; :: thesis: verum

end;

end;