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

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

suppose A2: ( 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, t be object ; :: according to FUNCT_1:def 4 :: 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 A3: ( 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
A4: ( (id X) . z = z & (id X) . t = t & (id X) . x = x & (id X) . y = y ) by A2, A3, FUNCT_1:17;
then A5: ( ( 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 A2, A1, Th29, Th31, Th33;
( ( 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 A2, A1, A4, Th29, Th31, Th33;
hence z = t by A3, A5; :: 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 A1, FUNCT_7:def 12; :: thesis: verum

end;

end;