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:12;
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:46
.= rng F by A2, FUNCT_1:12, ZFMISC_1:46 ;
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:12; :: 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:46
.= rng (Swap F,x,y) by A9, ZFMISC_1:46 ;
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;