let M, N be Cardinal; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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;
now :: thesis: for x being object st x in dom (Card f) holds
(Card f) . x c= ((dom f) --> N) . x
let x be object ; :: 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, CARD_3:def 2;
((dom f) --> N) . x = N by A4, A6, FUNCOP_1:7;
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, 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; :: thesis: verum