let x, y be set ; :: thesis: for X, Y being finite set st x <> y & X misses Y holds
(X --> x) +* (Y --> y) in Choose (X \/ Y),(card X),x,y
let X, Y be finite set ; :: thesis: ( x <> y & X misses Y implies (X --> x) +* (Y --> y) in Choose (X \/ Y),(card X),x,y )
assume A1: ( x <> y & X misses Y ) ; :: thesis: (X --> x) +* (Y --> y) in Choose (X \/ Y),(card X),x,y
( dom (X --> x) = X & dom (Y --> y) = Y ) by FUNCOP_1:19;
then (X --> x) +* (Y --> y) = (Y --> y) +* (X --> x) by A1, FUNCT_4:36;
hence (X --> x) +* (Y --> y) in Choose (X \/ Y),(card X),x,y by A1, Th19; :: thesis: verum