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;