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