>>528
|H| * |K| = # { (h, k) | h ∈ H, k ∈ K }
HK に於いて、
hk = h 'k ' ⇔ h^(-1)h ' = kk '^(-1) ∈ H ∩ K
より出る。