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