let F be Function; :: thesis: for x, y being object holds rng (Swap (F,x,y)) = rng F
let x, y be object ; :: 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 Th99, 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 Th31; :: thesis: verum

end;

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

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

end;

end;

end;

A5: rng F c= (rng (F +* (x,(F . y)))) \/ {(F . x)} by Th100;
A6: Swap (F,x,y) = (F +* (x,(F . y))) +* (y,(F . x)) by A1, A2, Def11;
then rng (Swap (F,x,y)) c= (rng (F +* (x,(F . y)))) \/ {(F . x)} by Th99;
then A7: rng (Swap (F,x,y)) c= rng F by A3;
A8: y in dom (F +* (x,(F . y))) by A2, Th29;
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, Th101; :: 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 Th98;
(Swap (F,x,y)) . x = (F +* (x,(F . y))) . x by A6, A10, Th31
.= F . y by A1, Th30 ;
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, Th101;
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, Th100, XBOOLE_1:9;
then rng F c= rng (Swap (F,x,y)) by A5;
hence rng (Swap (F,x,y)) = rng F by A7; :: 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 Def11; :: thesis: verum

end;

end;