let x, y, z be object ; :: thesis: for f being Function st z in dom f holds
swap ({(f . z)},x,y) = {((Swap (f,x,y)) . z)}
let f be Function; :: thesis: ( z in dom f implies swap ({(f . z)},x,y) = {((Swap (f,x,y)) . z)} )
assume A1: z in dom f ; :: thesis: swap ({(f . z)},x,y) = {((Swap (f,x,y)) . z)}

per cases ( x in f . z or not x in f . z ) ;

suppose x in f . z ; :: thesis: swap ({(f . z)},x,y) = {((Swap (f,x,y)) . z)}

then ( swap ({(f . z)},x,y) = {(((f . z) \ {x}) \/ {y})} & (Swap (f,x,y)) . z = ((f . z) \ {x}) \/ {y} ) by Def4, A1, Th31;
hence swap ({(f . z)},x,y) = {((Swap (f,x,y)) . z)} ; :: thesis: verum

end;

suppose not x in f . z ; :: thesis: swap ({(f . z)},x,y) = {((Swap (f,x,y)) . z)}

then ( swap ({(f . z)},x,y) = {((f . z) \/ {x})} & (f . z) \/ {x} = (Swap (f,x,y)) . z ) by A1, Def4, Th32;
hence swap ({(f . z)},x,y) = {((Swap (f,x,y)) . z)} ; :: thesis: verum

end;

end;