let k, n be Element of NAT ; :: thesis: for c', c being Element of COMPLEX
for z being Element of COMPLEX n st k in Seg n & c' = z . k holds
(c * z) . k = c * c'
let c', c be Element of COMPLEX ; :: thesis: for z being Element of COMPLEX n st k in Seg n & c' = z . k holds
(c * z) . k = c * c'
let z be Element of COMPLEX n; :: thesis: ( k in Seg n & c' = z . k implies (c * z) . k = c * c' )
assume that
A1: k in Seg n and
A2: c' = z . k ; :: thesis: (c * z) . k = c * c'
k in dom (c * z) by A1, Lm2;
hence (c * z) . k = (c multcomplex ) . c' by A2, FUNCT_1:22
.= c * c' by Lm1 ;
:: thesis: verum