let f be Function; ( dom f is finite & ( for x being object st x in dom f holds
f . x is finite ) implies Union f is finite )
assume that
A1:
dom f is finite
and
A2:
for x being object st x in dom f holds
f . x is finite
; Union f is finite
reconsider df = dom f as finite set by A1;
now ( dom f <> {} implies Union f is finite )assume
dom f <> {}
;
Union f is finite then A3:
df <> {}
;
defpred S1[
object ,
object ]
means card (f . $2) c= card (f . $1);
A4:
for
x,
y being
object holds
(
S1[
x,
y] or
S1[
y,
x] )
;
A5:
for
x,
y,
z being
object st
S1[
x,
y] &
S1[
y,
z] holds
S1[
x,
z]
by XBOOLE_1:1;
consider x being
object such that A6:
(
x in df & ( for
y being
object st
y in df holds
S1[
x,
y] ) )
from CARD_2:sch 2(A3, A4, A5);
reconsider fx =
f . x as
finite set by A2, A6;
A7:
card (Union f) c= (card (card df)) *` (card (f . x))
by A6, Th85;
card (f . x) = card (card fx)
;
then
card (Union f) c= card ((card df) * (card fx))
by A7, Th38;
hence
Union f is
finite
;
verum end;
hence
Union f is finite
by RELAT_1:42, ZFMISC_1:2; verum