let X be set ; :: thesis: for x, y being object st x in X & y in X holds
X \ {x},X \ {y} are_equipotent
let x, y be object ; :: thesis: ( x in X & y in X implies X \ {x},X \ {y} are_equipotent )
assume that
A1: x in X and
A2: y in X ; :: thesis: X \ {x},X \ {y} are_equipotent
defpred S1[ object , object ] means ( ( $1 = y & $2 = x ) or ( $1 <> y & $1 = $2 ) );
A3: for a being object st a in X \ {x} holds
ex b being object st S1[a,b]
proof
let a be object ; :: thesis: ( a in X \ {x} implies ex b being object st S1[a,b] )
assume a in X \ {x} ; :: thesis: ex b being object st S1[a,b]
( a = y implies ex b being object st S1[a,b] ) ;
hence ex b being object st S1[a,b] ; :: thesis: verum
end;
A4: for a, b1, b2 being object st a in X \ {x} & S1[a,b1] & S1[a,b2] holds
b1 = b2 ;
consider f being Function such that
A5: ( dom f = X \ {x} & ( for a being object st a in X \ {x} holds
S1[a,f . a] ) ) from FUNCT_1:sch 2(A4, A3);
 take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = X \ {x} & rng f = X \ {y} )
thus f is one-to-one :: thesis: ( dom f = X \ {x} & rng f = X \ {y} )
proof
let b1, b2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not b1 in dom f or not b2 in dom f or not f . b1 = f . b2 or b1 = b2 )
assume that
A6: ( b1 in dom f & b2 in dom f ) and
A7: ( f . b1 = f . b2 & b1 <> b2 ) ; :: thesis: contradiction
A8: ( not b1 in {x} & not b2 in {x} ) by A5, A6, XBOOLE_0:def 5;
( S1[b1,f . b1] & S1[b2,f . b2] ) by A5, A6;
hence contradiction by A7, A8, TARSKI:def 1; :: thesis: verum
end;
thus dom f = X \ {x} by A5; :: thesis: rng f = X \ {y}
thus rng f c= X \ {y} :: according to XBOOLE_0:def 10 :: thesis: X \ {y} c= rng f
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng f or z in X \ {y} )
assume z in rng f ; :: thesis: z in X \ {y}
then consider a being object such that
A9: a in dom f and
A10: z = f . a by FUNCT_1:def 3;
A11: now :: thesis: ( a = y implies z in X \ {y} )
assume A12: a = y ; :: thesis: z in X \ {y}
then ( not y in {x} & z = x ) by A5, A9, A10, XBOOLE_0:def 5;
then y <> z by TARSKI:def 1;
then A13: not z in {y} by TARSKI:def 1;
z in X by A1, A5, A9, A10, A12;
hence z in X \ {y} by A13, XBOOLE_0:def 5; :: thesis: verum
end;
now :: thesis: ( a <> y implies z in X \ {y} )
assume a <> y ; :: thesis: z in X \ {y}
then ( not a in {y} & a = z ) by A5, A9, A10, TARSKI:def 1;
hence z in X \ {y} by A5, A9, XBOOLE_0:def 5; :: thesis: verum
end;
hence z in X \ {y} by A11; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in X \ {y} or z in rng f )
assume A14: z in X \ {y} ; :: thesis: z in rng f
then not z in {y} by XBOOLE_0:def 5;
then A15: z <> y by TARSKI:def 1;
A16: now :: thesis: ( z <> x implies z in rng f )
assume z <> x ; :: thesis: z in rng f
then not z in {x} by TARSKI:def 1;
then A17: z in X \ {x} by A14, XBOOLE_0:def 5;
then z = f . z by A5, A15;
hence z in rng f by A5, A17, FUNCT_1:def 3; :: thesis: verum
end;
now :: thesis: ( z = x implies z in rng f )
assume A18: z = x ; :: thesis: z in rng f
then not y in {x} by A15, TARSKI:def 1;
then A19: y in dom f by A2, A5, XBOOLE_0:def 5;
then z = f . y by A5, A18;
hence z in rng f by A19, FUNCT_1:def 3; :: thesis: verum
end;
hence z in rng f by A16; :: thesis: verum