let k, n be Nat; :: thesis: for c, c9 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 c, c9 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, Lm4;
hence (c * z) . k = (c multcomplex) . c9 by A2, FUNCT_1:12
.= c * c9 by Lm3 ;
:: thesis: verum