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 that
A1: dom f is finite and
A2: for x being set st x in dom f holds
f . x is finite ; :: thesis: Union f is finite
reconsider df = dom f as finite set by A1;

now

assume dom f <> {} ; :: thesis: Union f is finite
then A3: df <> {} ;
defpred S₂[ set , set ] means card (f . $2) c= card (f . $1);
A4: for x, y being set holds
( S₂[x,y] or S₂[y,x] ) ;
A5: for x, y, z being set st S₂[x,y] & S₂[y,z] holds
S₂[x,z] by XBOOLE_1:1;
consider x being set such that
A6: ( x in df & ( for y being set st y in df holds
S₂[x,y] ) ) from CARD_3:sch 3(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, Th132;
card (f . x) = card (card fx) ;
then card (Union f) c= card ((card df) * (card fx)) by A7, 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