let M, N be Cardinal; for f being Function st card (dom f) c= M & ( for x being object st x in dom f holds
card (f . x) c= N ) holds
card (Union f) c= M *` N
let f be Function; ( card (dom f) c= M & ( for x being object st x in dom f holds
card (f . x) c= N ) implies card (Union f) c= M *` N )
assume that
A1:
card (dom f) c= M
and
A2:
for x being object st x in dom f holds
card (f . x) c= N
; card (Union f) c= M *` N
A3:
card (Union f) c= Sum (Card f)
by CARD_3:39;
A4:
dom (Card f) = dom f
by CARD_3:def 2;
A5:
dom ((dom f) --> N) = dom f
by FUNCOP_1:13;
then
Sum (Card f) c= Sum ((dom f) --> N)
by A4, A5, CARD_3:30;
then A8:
card (Union f) c= Sum ((dom f) --> N)
by A3;
A9:
[:(card (dom f)),N:] c= [:M,N:]
by A1, ZFMISC_1:95;
Sum ((dom f) --> N) =
card [:N,(dom f):]
by CARD_3:25
.=
card [:N,(card (dom f)):]
by Th6
.=
card [:(card (dom f)),N:]
by Th4
;
then A10:
Sum ((dom f) --> N) c= card [:M,N:]
by A9, CARD_1:11;
thus
card (Union f) c= M *` N
by A8, A10; verum