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