let x, y be set ; :: thesis: for f being Function st x in dom f & y in dom f holds
Swap (f,x,y) = Swap (f,y,x)
let f be Function; :: thesis: ( x in dom f & y in dom f implies Swap (f,x,y) = Swap (f,y,x) )
assume Z0: ( x in dom f & y in dom f ) ; :: thesis: Swap (f,x,y) = Swap (f,y,x)
A0: ( dom (Swap (f,x,y)) = dom f & dom (Swap (f,y,x)) = dom f ) by FUNCT_7:99;

now

let z be set ; :: thesis: ( z in dom f implies (Swap (f,x,y)) . b₁ = (Swap (f,y,x)) . b₁ )
assume z in dom f ; :: thesis: (Swap (f,x,y)) . b₁ = (Swap (f,y,x)) . b₁

per cases ( ( z = x & z = y ) or ( z = x & z <> y ) or ( z <> x & z = y ) or ( z <> x & z <> y ) ) ;

suppose ( z = x & z = y ) ; :: thesis: (Swap (f,x,y)) . b₁ = (Swap (f,y,x)) . b₁

hence (Swap (f,x,y)) . z = (Swap (f,y,x)) . z ; :: thesis: verum

end;

suppose ( z = x & z <> y ) ; :: thesis: (Swap (f,x,y)) . b₁ = (Swap (f,y,x)) . b₁

then ( (Swap (f,x,y)) . z = f . y & (Swap (f,y,x)) . z = f . y ) by Z0, TSa, TSb;
hence (Swap (f,x,y)) . z = (Swap (f,y,x)) . z ; :: thesis: verum

end;

suppose ( z <> x & z = y ) ; :: thesis: (Swap (f,x,y)) . b₁ = (Swap (f,y,x)) . b₁

then ( (Swap (f,x,y)) . z = f . x & (Swap (f,y,x)) . z = f . x ) by Z0, TSa, TSb;
hence (Swap (f,x,y)) . z = (Swap (f,y,x)) . z ; :: thesis: verum

end;

suppose ( z <> x & z <> y ) ; :: thesis: (Swap (f,x,y)) . b₁ = (Swap (f,y,x)) . b₁

then ( (Swap (f,x,y)) . z = f . z & (Swap (f,y,x)) . z = f . z ) by TSc;
hence (Swap (f,x,y)) . z = (Swap (f,y,x)) . z ; :: thesis: verum

end;

end;

end;

hence Swap (f,x,y) = Swap (f,y,x) by A0, FUNCT_1:2; :: thesis: verum