let i be Element of NAT ; :: thesis: for x being FinSequence of COMPLEX holds (- x) . i = - (x . i)
let x be FinSequence of COMPLEX ; :: thesis: (- x) . i = - (x . i)

per cases ( not i in dom (- x) or i in dom (- x) ) ;

suppose A1: not i in dom (- x) ; :: thesis: (- x) . i = - (x . i)

then A2: not i in dom x by VALUED_1:8;
thus (- x) . i = - 0 by A1, FUNCT_1:def 2
.= - (x . i) by A2, FUNCT_1:def 2 ; :: thesis: verum

end;

suppose A3: i in dom (- x) ; :: thesis: (- x) . i = - (x . i)

set r = x . i;
- x = compcomplex * x by SEQ_4:def 8;
then (- x) . i = compcomplex . (x . i) by A3, FUNCT_1:12;
hence (- x) . i = - (x . i) by BINOP_2:def 1; :: thesis: verum

end;

end;