let f be complex-valued FinSequence; :: thesis: ( f - f = 0 (#) f & f - f = (len f) |-> 0 )
f - f = f + (- f) by VALUED_1:def 9
.= (1 (#) f) + ((- 1) (#) f) by VALUED_1:def 6
.= (1 + (- 1)) (#) f by TOPREALC:2
.= 0 (#) f ;
hence ( f - f = 0 (#) f & f - f = (len f) |-> 0 ) by EMP; :: thesis: verum