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