let M, N be Cardinal; :: thesis: for f being Function st card (dom f) c= M & ( for x being set st x in dom f holds
card (f . x) c= N ) holds
card (Union f) c= M *` N
let f be Function; :: thesis: ( card (dom f) c= M & ( for x being set 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 set st x in dom f holds
card (f . x) c= N ; :: thesis: card (Union f) c= M *` N
A3: card (Union f) c= Sum (Card f) by Th54;
A4: dom (Card f) = dom f by Def2;
A5: dom ((dom f) --> N) = dom f by FUNCOP_1:19;

now

let x be set ; :: thesis: ( x in dom (Card f) implies (Card f) . x c= ((dom f) --> N) . x )
assume A6: x in dom (Card f) ; :: thesis: (Card f) . x c= ((dom f) --> N) . x
then A7: (Card f) . x = card (f . x) by A4, Def2;
((dom f) --> N) . x = N by A4, A6, FUNCOP_1:13;
hence (Card f) . x c= ((dom f) --> N) . x by A2, A4, A6, A7; :: thesis: verum

end;

then Sum (Card f) c= Sum ((dom f) --> N) by A4, A5, Th43;
then A8: card (Union f) c= Sum ((dom f) --> N) by A3, XBOOLE_1:1;
A9: [:(card (dom f)),N:] c= [:M,N:] by A1, ZFMISC_1:118;
Sum ((dom f) --> N) = card [:N,(dom f):] by Th36
.= card [:N,(card (dom f)):] by CARD_2:14
.= card [:(card (dom f)),N:] by CARD_2:11 ;
then A10: Sum ((dom f) --> N) c= card [:M,N:] by A9, CARD_1:27;
card [:M,N:] = M *` N by CARD_2:def 2;
hence card (Union f) c= M *` N by A8, A10, XBOOLE_1:1; :: thesis: verum