let f be Function; :: thesis: ( 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 ; :: thesis: Union f is finite
reconsider df = dom f as finite set by A1;
now :: thesis: ( dom f <> {} implies Union f is finite )
assume dom f <> {} ; :: thesis: 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 ; :: thesis: verum
end;
hence Union f is finite by RELAT_1:42, ZFMISC_1:2; :: thesis: verum