let X, Y be finite set ; :: thesis: for x, y being object st x <> y holds
(Y --> y) +* (X --> x) in Choose ((X \/ Y),(card X),x,y)
let x, y be object ; :: thesis: ( x <> y implies (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 ) ;
then A1: dom ((Y --> y) +* (X --> x)) = X \/ Y by FUNCT_4:def 1;
{y} c= {x,y} by ZFMISC_1:7;
then A2: rng (Y --> y) c= {x,y} ;
{x} c= {x,y} by ZFMISC_1:7;
then rng (X --> x) c= {x,y} ;
then ( rng ((Y --> y) +* (X --> x)) c= (rng (X --> x)) \/ (rng (Y --> y)) & (rng (X --> x)) \/ (rng (Y --> y)) c= {x,y} ) by A2, FUNCT_4:17, XBOOLE_1:8;
then reconsider F = (Y --> y) +* (X --> x) as Function of (X \/ Y),{x,y} by A1, FUNCT_2:2, XBOOLE_1:1;
assume A3: x <> y ; :: thesis: (Y --> y) +* (X --> x) in Choose ((X \/ Y),(card X),x,y)
A4: F " {x} c= X
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in F " {x} or z in X )
assume A5: z in F " {x} ; :: thesis: z in X
A6: ( z in X or z in Y ) by A5, XBOOLE_0:def 3;
F . z in {x} by A5, FUNCT_1:def 7;
then A7: F . z = x by TARSKI:def 1;
z in dom F by A5, FUNCT_1:def 7;
then A8: z in (dom (X --> x)) \/ (dom (Y --> y)) ;
assume A9: not z in X ; :: thesis: contradiction
F . z = (Y --> y) . z by A9, A8, FUNCT_4:def 1;
hence contradiction by A3, A9, A6, A7, FUNCOP_1:7; :: thesis: verum
end;
X c= F " {x}
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in X or z in F " {x} )
assume A10: z in X ; :: thesis: z in F " {x}
A11: z in dom F by A1, A10, XBOOLE_0:def 3;
z in dom (X --> x) by A10;
then A12: F . z = (X --> x) . z by FUNCT_4:13;
(X --> x) . z = x by A10, FUNCOP_1:7;
then F . z in {x} by A12, TARSKI:def 1;
hence z in F " {x} by A11, FUNCT_1:def 7; :: thesis: verum
end;
then X = F " {x} by A4;
hence (Y --> y) +* (X --> x) in Choose ((X \/ Y),(card X),x,y) by Def1; :: thesis: verum