let U be Universe; :: thesis: for x being Element of U holds comp (Trivial-addLoopStr x) is Element of U
let x be Element of U; :: thesis: comp (Trivial-addLoopStr x) is Element of U
set Tx = Trivial-addLoopStr x;
{x} is Element of U ;
then reconsider y = the carrier of (Trivial-addLoopStr x) as Element of U ;
[:y,y:] is Element of U ;
hence comp (Trivial-addLoopStr x) is Element of U by CLASSES4:13; :: thesis: verum