let X be set ; :: thesis: for F being Function
for x, y being object st not x in X & not y in X holds
F | X = (Swap (F,x,y)) | X
let F be Function; :: thesis: for x, y being object st not x in X & not y in X holds
F | X = (Swap (F,x,y)) | X
let x, y be object ; :: thesis: ( not x in X & not y in X implies F | X = (Swap (F,x,y)) | X )
assume A1: ( not x in X & not y in X ) ; :: thesis: F | X = (Swap (F,x,y)) | X
dom F = dom (Swap (F,x,y)) by FUNCT_7:99;
then dom (F | X) = (dom (Swap (F,x,y))) /\ X by RELAT_1:61;
then A2: dom (F | X) = dom ((Swap (F,x,y)) | X) by RELAT_1:61;
now :: thesis: for z being object st z in dom (F | X) holds
(F | X) . z = ((Swap (F,x,y)) | X) . z
let z be object ; :: thesis: ( z in dom (F | X) implies (F | X) . z = ((Swap (F,x,y)) | X) . z )
assume z in dom (F | X) ; :: thesis: (F | X) . z = ((Swap (F,x,y)) | X) . z
then A3: z in X by RELAT_1:57;
then (Swap (F,x,y)) . z = F . z by A1, EXCHSORT:33;
then (F | X) . z = (Swap (F,x,y)) . z by A3, FUNCT_1:49;
hence (F | X) . z = ((Swap (F,x,y)) | X) . z by A3, FUNCT_1:49; :: thesis: verum
end;
hence F | X = (Swap (F,x,y)) | X by A2, FUNCT_1:2; :: thesis: verum