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