let X be set ; :: thesis: for M, N being Cardinal st X is mutually-disjoint & M c= card X & ( for Y being set st Y in X holds
N c= card Y ) holds
M *` N c= card (union X)
let M, N be Cardinal; :: thesis: ( X is mutually-disjoint & M c= card X & ( for Y being set st Y in X holds
N c= card Y ) implies M *` N c= card (union X) )
assume that
A1: X is mutually-disjoint and
A2: M c= card X and
A3: for Y being set st Y in X holds
N c= card Y ; :: thesis: M *` N c= card (union X)

now :: thesis: for x being object st x in dom (id X) holds
N c= card ((id X) . x)

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

end;

then M *` N c= Sum (Card (id X)) by A2, Th12;
hence M *` N c= card (union X) by A1, Th14; :: thesis: verum