let A, B be Ordinal; :: thesis: card (A *^ B) = (card A) *` (card B)
thus card (A *^ B) = card [:A,B:] by Th10
.= (card A) *` (card B) by Th6 ; :: thesis: verum