let a, b be Element of Trivial-multLoopStr; :: thesis: ex x being Element of Trivial-multLoopStr st a * x = b
take 1_ Trivial-multLoopStr ; :: thesis: a * (1_ Trivial-multLoopStr) = b
thus a * (1_ Trivial-multLoopStr) = b by Th9; :: thesis: verum