let D be non empty set ; :: thesis: for a, b being Element of (D *+^+<0>) holds a [*] b = a ^ b
let a, b be Element of (D *+^+<0>); :: thesis: a [*] b = a ^ b
multMagma(# the carrier of (D *+^+<0>), the multF of (D *+^+<0>) #) = D *+^ by Def22;
then reconsider p = a, q = b as Element of (D *+^) ;
thus a [*] b = p [*] q by Th18
.= a ^ b by Def34 ; :: thesis: verum