reconsider f = comp Trivial-addLoopStr as Function of {{} },{{} } by CARD_1:87;
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:87;
x = {} by CARD_1:87, TARSKI:def 1;
then op1 . x = - x by Th5, CARD_1:87, TARSKI:def 1
.= f . x by VECTSP_1:def 25 ;
hence op1 . x = f . x ; :: thesis: verum

end;

hence comp Trivial-addLoopStr = op1 by CARD_1:87, FUNCT_2:18; :: thesis: verum