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