let M, N be Cardinal; :: thesis: for X being set st card X c= M & ( for Y being set st Y in X holds
card Y c= N ) holds
card (union X) c= M *` N
let X be set ; :: thesis: ( card X c= M & ( for Y being set st Y in X holds
card Y c= N ) implies card (union X) c= M *` N )
assume that
A1: card X c= M and
A2: for Y being set st Y in X holds
card Y c= N ; :: thesis: card (union X) c= M *` N
A3: dom (id X) = X by RELAT_1:45;

now

let x be set ; :: thesis: ( x in dom (id X) implies card ((id X) . x) c= N )
assume x in dom (id X) ; :: thesis: card ((id X) . x) c= N
then (id X) . x in X by A3, FUNCT_1:18;
hence card ((id X) . x) c= N by A2; :: thesis: verum

end;

then card (Union (id X)) c= M *` N by A1, A3, Th132;
hence card (union X) c= M *` N by RELAT_1:45; :: thesis: verum