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