let K, M be Cardinal; :: thesis: exp ((K +` M),2) = ((K *` K) +` ((2 *` K) *` M)) +` (M *` M)
thus exp ((K +` M),2) = (K +` M) *` (K +` M) by CARD_1:50, FUNCT_5:66
.= (K *` (K +` M)) +` (M *` (K +` M)) by Th23
.= ((K *` K) +` (K *` M)) +` (M *` (K +` M)) by Th23
.= ((K *` K) +` (K *` M)) +` ((M *` K) +` (M *` M)) by Th23
.= (((K *` K) +` (K *` M)) +` (K *` M)) +` (M *` M) by Th18
.= ((K *` K) +` ((K *` M) +` (K *` M))) +` (M *` M) by Th18
.= ((K *` K) +` (2 *` (K *` M))) +` (M *` M) by Th22
.= ((K *` K) +` ((2 *` K) *` M)) +` (M *` M) by Th21 ; :: thesis: verum