let K, M, N be Cardinal; :: thesis: (K *` M) *` N = K *` (M *` N)
thus (K *` M) *` N = card [:[:K,M:],N:] by Th6
.= card [:K,[:M,N:]:] by Th5
.= K *` (M *` N) by Th6 ; :: thesis: verum