let x, y be set ; :: thesis: for Y, X being finite set st x <> y holds
(Y --> y) +* (X --> x) in Choose (X \/ Y),(card X),x,y
let Y, X be finite set ; :: thesis: ( x <> y implies (Y --> y) +* (X --> x) in Choose (X \/ Y),(card X),x,y )
assume A1: x <> y ; :: thesis: (Y --> y) +* (X --> x) in Choose (X \/ Y),(card X),x,y
set F = (Y --> y) +* (X --> x);
( dom (Y --> y) = Y & dom (X --> x) = X & rng (X --> x) c= {x} & rng (Y --> y) c= {y} & {x} c= {x,y} & {y} c= {x,y} ) by FUNCOP_1:19, ZFMISC_1:12;
then A2: ( dom ((Y --> y) +* (X --> x)) = X \/ Y & rng (X --> x) c= {x,y} & rng (Y --> y) c= {x,y} ) by FUNCT_4:def 1, XBOOLE_1:1;
then ( dom ((Y --> y) +* (X --> x)) = X \/ Y & rng ((Y --> y) +* (X --> x)) c= (rng (X --> x)) \/ (rng (Y --> y)) & (rng (X --> x)) \/ (rng (Y --> y)) c= {x,y} ) by FUNCT_4:18, XBOOLE_1:8;
then reconsider F = (Y --> y) +* (X --> x) as Function of (X \/ Y),{x,y} by FUNCT_2:4, XBOOLE_1:1;
A3: F " {x} c= X

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in F " {x} or z in X )
assume A4: z in F " {x} ; :: thesis: z in X
assume A5: not z in X ; :: thesis: contradiction
z in dom F by A4, FUNCT_1:def 13;
then ( ( z in X or z in Y ) & z in (dom (X --> x)) \/ (dom (Y --> y)) & X = dom (X --> x) & F . z in {x} ) by A4, FUNCOP_1:19, FUNCT_1:def 13, FUNCT_4:def 1, XBOOLE_0:def 3;
then ( z in Y & F . z = (Y --> y) . z & F . z = x ) by A5, FUNCT_4:def 1, TARSKI:def 1;
hence contradiction by A1, FUNCOP_1:13; :: thesis: verum

end;

X c= F " {x}

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in X or z in F " {x} )
assume A6: z in X ; :: thesis: z in F " {x}
z in dom (X --> x) by A6, FUNCOP_1:19;
then ( F . z = (X --> x) . z & (X --> x) . z = x ) by FUNCOP_1:13, FUNCT_4:14;
then ( F . z in {x} & z in dom F ) by A2, A6, TARSKI:def 1, XBOOLE_0:def 3;
hence z in F " {x} by FUNCT_1:def 13; :: thesis: verum

end;

then X = F " {x} by A3, XBOOLE_0:def 10;
hence (Y --> y) +* (X --> x) in Choose (X \/ Y),(card X),x,y by Def1; :: thesis: verum