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 that
A1: x <> y and
A2: X misses Y ; :: thesis: (X --> x) +* (Y --> y) in Choose ((X \/ Y),(card X),x,y)
( dom (X --> x) = X & dom (Y --> y) = Y ) ;
then (X --> x) +* (Y --> y) = (Y --> y) +* (X --> x) by A2, FUNCT_4:35;
hence (X --> x) +* (Y --> y) in Choose ((X \/ Y),(card X),x,y) by A1, Th16; :: thesis: verum