let x be object ; :: according to HILB10_7:def 7 :: thesis: ( x in X \/ Y implies x is finite with_evenly_repeated_values Function )
assume x in X \/ Y ; :: thesis: x is finite with_evenly_repeated_values Function
then ( x in X or x in Y ) by XBOOLE_0:def 3;
hence x is finite with_evenly_repeated_values Function ; :: thesis: verum