reconsider f = comp Trivial-addLoopStr as Function of {{}},{{}} ;
for x being object st x in {{}} holds
op1 . x = f . x

proof

let x be object ; :: thesis: ( x in {{}} implies op1 . x = f . x )
assume x in {{}} ; :: thesis: op1 . x = f . x
then reconsider x = x as Element of Trivial-addLoopStr ;
x = {} by TARSKI:def 1;
then op1 . x = - x by Th2, TARSKI:def 1
.= f . x by VECTSP_1:def 13 ;
hence op1 . x = f . x ; :: thesis: verum

end;

hence comp Trivial-addLoopStr = op1 by FUNCT_2:12; :: thesis: verum