theorem Th25: :: MONOID_0:25

for G being non empty multMagma
for H being non empty SubStr of G
for a, b being Element of H
for a9, b9 being Element of G st a = a9 & b = b9 holds
a * b = a9 * b9