reconsider f = comp Trivial-addLoopStr as Function of {{}},{{}} by CARD_1:49;
for x being set st x in {{}} holds
op1 . x = f . x

proof

let x be set ; :: 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 by CARD_1:49;
x = {} by CARD_1:49, TARSKI:def 1;
then op1 . x = - x by Th5, CARD_1:49, TARSKI:def 1
.= f . x by VECTSP_1:def 13 ;
hence op1 . x = f . x ; :: thesis: verum

end;

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