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 Th20
.= a ^ b by Def34 ; :: thesis: verum