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
for x being object st x in dom f holds
card (f . x) c= omega by A2, CARD_3:def 14;
hence card (Union f) c= omega by A1, Th6, CARD_2:86; :: according to CARD_3:def 14 :: thesis: verum