let k, n be Nat; :: thesis: for c being Element of COMPLEX
for z being Element of COMPLEX n st k in Seg n & c = z . k holds
(- z) . k = - c
let c be Element of COMPLEX ; :: thesis: for z being Element of COMPLEX n st k in Seg n & c = z . k holds
(- z) . k = - c
let z be Element of COMPLEX n; :: thesis: ( k in Seg n & c = z . k implies (- z) . k = - c )
assume that
A1: k in Seg n and
A2: c = z . k ; :: thesis: (- z) . k = - c
k in dom (- z) by A1, Lm4;
hence (- z) . k = compcomplex . c by A2, FUNCT_1:12
.= - c by BINOP_2:def 1 ;
:: thesis: verum