theorem Th63: :: MONOID_0:63

for D being set
for F being non empty SubStr of D *+^
for p, q being Element of F holds p [*] q = p ^ q