for a, b being Element of Trivial-multLoopStr holds a * b = 1. Trivial-multLoopStr by Th9;