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

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