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