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