let F be Function; :: thesis: 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 ; :: thesis: ( 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 ) ; :: thesis: 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 :: thesis: 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))) . z

let z be object ; :: thesis: ( 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)) ; :: thesis: (Swap (F,x,y)) . z = (F * (Swap ((id (dom F)),x,y))) . z

A6: now :: thesis: ( z = x implies (Swap (F,x,y)) . z = (F * (Swap ((id (dom F)),x,y))) . z )

assume A7: z = x ; :: thesis: (Swap (F,x,y)) . z = (F * (Swap ((id (dom F)),x,y))) . z
then 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; :: thesis: verum

end;

A9: now :: thesis: ( z = y implies (Swap (F,x,y)) . z = (F * (Swap ((id (dom F)),x,y))) . z )

assume A10: z = y ; :: thesis: (Swap (F,x,y)) . z = (F * (Swap ((id (dom F)),x,y))) . z
then 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; :: thesis: verum

end;

now :: thesis: ( z <> x & z <> y implies (Swap (F,x,y)) . z = (F * (Swap ((id (dom F)),x,y))) . z )

assume A12: ( z <> x & z <> y ) ; :: thesis: (Swap (F,x,y)) . z = (F * (Swap ((id (dom F)),x,y))) . z
then 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; :: thesis: verum

end;

hence (Swap (F,x,y)) . z = (F * (Swap ((id (dom F)),x,y))) . z by A6, A9; :: thesis: verum

end;

hence Swap (F,x,y) = F * (Swap ((id (dom F)),x,y)) by A3, FUNCT_1:def 11; :: thesis: verum