let f be Function; :: thesis: ( dom f is countable & ( for x being set st x in dom f holds
f . x is countable ) implies Union f is countable )
assume A1: ( card (dom f) c= omega & ( for x being set st x in dom f holds
f . x is countable ) ) ; :: according to CARD_3:def 15 :: thesis: Union f is countable

now

let x be set ; :: thesis: ( x in dom f implies card (f . x) c= omega )
assume x in dom f ; :: thesis: card (f . x) c= omega
then f . x is countable by A1;
hence card (f . x) c= omega by CARD_3:def 15; :: thesis: verum

end;

hence card (Union f) c= omega by A1, Th54, CARD_3:132; :: according to CARD_3:def 15 :: thesis: verum