let F be Function; for x, y being object st x in dom F & y in dom F holds
Swap (F,x,y) = F * (Swap ((id (dom F)),x,y))
let x, y be object ; ( x in dom F & y in dom F implies Swap (F,x,y) = F * (Swap ((id (dom F)),x,y)) )
assume A1:
( x in dom F & y in dom F )
; Swap (F,x,y) = F * (Swap ((id (dom F)),x,y))
A2:
( dom (Swap (F,x,y)) = dom F & dom (Swap ((id (dom F)),x,y)) = dom (id (dom F)) )
by FUNCT_7:99;
rng (Swap ((id (dom F)),x,y)) = rng (id (dom F))
by FUNCT_7:103;
then A3:
dom (F * (Swap ((id (dom F)),x,y))) = dom (Swap (F,x,y))
by A2, RELAT_1:27;
A4:
dom (id (dom F)) = dom F
;
now for z being object st z in dom (Swap (F,x,y)) holds
(Swap (F,x,y)) . z = (F * (Swap ((id (dom F)),x,y))) . zlet z be
object ;
( z in dom (Swap (F,x,y)) implies (Swap (F,x,y)) . z = (F * (Swap ((id (dom F)),x,y))) . z )assume A5:
z in dom (Swap (F,x,y))
;
(Swap (F,x,y)) . z = (F * (Swap ((id (dom F)),x,y))) . zA6:
now ( z = x implies (Swap (F,x,y)) . z = (F * (Swap ((id (dom F)),x,y))) . z )assume A7:
z = x
;
(Swap (F,x,y)) . z = (F * (Swap ((id (dom F)),x,y))) . zthen A8:
(Swap (F,x,y)) . z = F . y
by A1, EXCHSORT:29;
(Swap ((id (dom F)),x,y)) . z = (id (dom F)) . y
by A1, A4, A7, EXCHSORT:29;
then
(Swap ((id (dom F)),x,y)) . z = y
by A1, FUNCT_1:18;
hence
(Swap (F,x,y)) . z = (F * (Swap ((id (dom F)),x,y))) . z
by A1, A2, A7, A8, FUNCT_1:13;
verum end; A9:
now ( z = y implies (Swap (F,x,y)) . z = (F * (Swap ((id (dom F)),x,y))) . z )assume A10:
z = y
;
(Swap (F,x,y)) . z = (F * (Swap ((id (dom F)),x,y))) . zthen A11:
(Swap (F,x,y)) . z = F . x
by A1, EXCHSORT:31;
(Swap ((id (dom F)),x,y)) . z = (id (dom F)) . x
by A1, A4, A10, EXCHSORT:31;
then
(Swap ((id (dom F)),x,y)) . z = x
by A1, FUNCT_1:18;
hence
(Swap (F,x,y)) . z = (F * (Swap ((id (dom F)),x,y))) . z
by A1, A2, A10, A11, FUNCT_1:13;
verum end; now ( z <> x & z <> y implies (Swap (F,x,y)) . z = (F * (Swap ((id (dom F)),x,y))) . z )assume A12:
(
z <> x &
z <> y )
;
(Swap (F,x,y)) . z = (F * (Swap ((id (dom F)),x,y))) . zthen A13:
(Swap (F,x,y)) . z = F . z
by EXCHSORT:33;
(Swap ((id (dom F)),x,y)) . z =
(id (dom F)) . z
by A12, EXCHSORT:33
.=
z
by A2, A5, FUNCT_1:18
;
hence
(Swap (F,x,y)) . z = (F * (Swap ((id (dom F)),x,y))) . z
by A2, A5, A13, FUNCT_1:13;
verum end; hence
(Swap (F,x,y)) . z = (F * (Swap ((id (dom F)),x,y))) . z
by A6, A9;
verum end;
hence
Swap (F,x,y) = F * (Swap ((id (dom F)),x,y))
by A3, FUNCT_1:def 11; verum