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 A1: ( x in dom f & y in dom f ) ; :: thesis: Swap (f,x,y) = Swap (f,y,x)
A2: ( dom (Swap (f,x,y)) = dom f & dom (Swap (f,y,x)) = dom f ) by FUNCT_7:99;

now :: thesis: for z being object st z in dom f holds
(Swap (f,x,y)) . z = (Swap (f,y,x)) . z

let z be object ; :: 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 A1, Th29, Th31;
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 A1, Th29, Th31;
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 Th33;
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 A2; :: thesis: verum