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
now :: thesis: for x being object st x in dom (id X) holds
card ((id X) . x) c= N
let x be object ; :: 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 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, Th85;
hence card (union X) c= M *` N ; :: thesis: verum