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 that
A1: card (dom f) c= omega and
A2: for x being set st x in dom f holds
f . x is countable ; :: according to CARD_3:def 14 :: 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 A2;
hence card (f . x) c= omega by CARD_3:def 14; :: thesis: verum

end;

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