let M, N be Cardinal; :: thesis: for f being Function st M c= card (dom f) & ( for x being object st x in dom f holds
N c= card (f . x) ) holds
M *` N c= Sum (Card f)
let f be Function; :: thesis: ( M c= card (dom f) & ( for x being object st x in dom f holds
N c= card (f . x) ) implies M *` N c= Sum (Card f) )
assume that
A1: M c= card (dom f) and
A2: for x being object st x in dom f holds
N c= card (f . x) ; :: thesis: M *` N c= Sum (Card f)
A3: dom (Card f) = dom f by CARD_3:def 2;
A4: dom ((dom f) --> N) = dom f ;

now :: thesis: for x being object st x in dom (Card f) holds
((dom f) --> N) . x c= (Card f) . x

let x be object ; :: thesis: ( x in dom (Card f) implies ((dom f) --> N) . x c= (Card f) . x )
assume A5: x in dom (Card f) ; :: thesis: ((dom f) --> N) . x c= (Card f) . x
then A6: (Card f) . x = card (f . x) by A3, CARD_3:def 2;
((dom f) --> N) . x = N by A3, A5, FUNCOP_1:7;
hence ((dom f) --> N) . x c= (Card f) . x by A2, A3, A5, A6; :: thesis: verum

end;

then A7: Sum ((dom f) --> N) c= Sum (Card f) by A3, A4, CARD_3:30;
A8: [:M,N:] c= [:(card (dom f)),N:] by A1, ZFMISC_1:95;
Sum ((dom f) --> N) = card (Union (disjoin ((dom f) --> N))) by CARD_3:def 7
.= card [:N,(dom f):] by CARD_3:25
.= card [:N,(card (dom f)):] by CARD_2:7
.= card [:(card (dom f)),N:] by CARD_2:4 ;
then card [:M,N:] c= Sum ((dom f) --> N) by A8, CARD_1:11;
then card [:M,N:] c= Sum (Card f) by A7, XBOOLE_1:1;
hence M *` N c= Sum (Card f) by CARD_2:def 2; :: thesis: verum