let a, b be Element of Trivial-addLoopStr; :: thesis: ex x being Element of Trivial-addLoopStr st a + x = b
take 0. Trivial-addLoopStr ; :: thesis: a + (0. Trivial-addLoopStr) = b
thus a + (0. Trivial-addLoopStr) = b by Th4; :: thesis: verum