let f be non-empty disjoint_valued Function; :: thesis: ( Union f is finite implies dom f is finite )
assume Union f is finite ; :: thesis: dom f is finite
then A1: ( rng f is finite & ( for X being set st X in rng f holds
X is finite ) ) by FINSET_1:7;
for x, y being object st x in dom f & y in dom f & f . x = f . y holds
x = y
proof
let x, y be object ; :: thesis: ( x in dom f & y in dom f & f . x = f . y implies x = y )
assume A2: ( x in dom f & y in dom f & f . x = f . y ) ; :: thesis: x = y
assume x <> y ; :: thesis: contradiction
then A3: (f . x) /\ (f . y) = {} by PROB_2:def 2, XBOOLE_0:def 7;
f . x in rng f by A2, FUNCT_1:3;
then consider i being object such that
A4: i in f . x by XBOOLE_0:def 1;
thus contradiction by A2, A3, A4; :: thesis: verum
end;
then f is one-to-one ;
hence dom f is finite by A1, CARD_1:59; :: thesis: verum