let X, x, y be set ; :: thesis: Swap ((id X),x,y) is one-to-one
A0: dom (id X) = X by RELAT_1:45;

per cases ( ( x in X & y in X ) or not x in X or not y in X ) ;

suppose Z0: ( x in X & y in X ) ; :: thesis: Swap ((id X),x,y) is one-to-one

set g = id X;
set f = Swap ((id X),x,y);
let z be set ; :: according to FUNCT_1:def 4 :: thesis: for b₁ being set holds
( not z in proj1 (Swap ((id X),x,y)) or not b₁ in proj1 (Swap ((id X),x,y)) or not (Swap ((id X),x,y)) . z = (Swap ((id X),x,y)) . b₁ or z = b₁ )
let t be set ; :: thesis: ( not z in proj1 (Swap ((id X),x,y)) or not t in proj1 (Swap ((id X),x,y)) or not (Swap ((id X),x,y)) . z = (Swap ((id X),x,y)) . t or z = t )
assume Z1: ( z in dom (Swap ((id X),x,y)) & t in dom (Swap ((id X),x,y)) & (Swap ((id X),x,y)) . z = (Swap ((id X),x,y)) . t ) ; :: thesis: z = t
dom (Swap ((id X),x,y)) = X by A0, FUNCT_7:99;
then A2: ( (id X) . z = z & (id X) . t = t & (id X) . x = x & (id X) . y = y ) by Z0, Z1, FUNCT_1:17;
then A3: ( ( z = x implies (Swap ((id X),x,y)) . z = y ) & ( z = y implies (Swap ((id X),x,y)) . z = x ) & ( z <> x & z <> y implies (Swap ((id X),x,y)) . z = z ) ) by Z0, A0, TSa, TSb, TSc;
( ( t = x implies (Swap ((id X),x,y)) . t = y ) & ( t = y implies (Swap ((id X),x,y)) . t = x ) & ( t <> x & t <> y implies (Swap ((id X),x,y)) . t = t ) ) by Z0, A0, A2, TSa, TSb, TSc;
hence z = t by Z1, A3; :: thesis: verum

end;

suppose ( not x in X or not y in X ) ; :: thesis: Swap ((id X),x,y) is one-to-one

hence Swap ((id X),x,y) is one-to-one by A0, FUNCT_7:def 12; :: thesis: verum

end;

end;