let H, K be finite Group; :: thesis: card (product <*H,K*>) = (card H) * (card K)
card (product <* the carrier of H, the carrier of K*>) = card the carrier of (product <*H,K*>) by Th10;
hence card (product <*H,K*>) = (card H) * (card K) by Th2; :: thesis: verum