set g = (c multcomplex) * z;
dom (c multcomplex) = COMPLEX by FUNCT_2:def 1;
then rng z c= dom (c multcomplex) ;
then A1: ( dom (c (#) z) = dom z & dom ((c multcomplex) * z) = dom z ) by RELAT_1:27, VALUED_1:def 5;

now :: thesis: for x being object st x in dom (c (#) z) holds
(c (#) z) . x = ((c multcomplex) * z) . x

let x be object ; :: thesis: ( x in dom (c (#) z) implies (c (#) z) . x = ((c multcomplex) * z) . x )
assume A2: x in dom (c (#) z) ; :: thesis: (c (#) z) . x = ((c multcomplex) * z) . x
A3: ( c is Element of COMPLEX & z . x is Element of COMPLEX ) by XCMPLX_0:def 2;
thus (c (#) z) . x = c * (z . x) by VALUED_1:6
.= (c multcomplex) . (z . x) by A3, Lm3
.= ((c multcomplex) * z) . x by A1, A2, FUNCT_1:12 ; :: thesis: verum

end;

hence for b₁ being FinSequence of COMPLEX holds
( b₁ = c * z iff b₁ = (c multcomplex) * z ) by A1, FUNCT_1:2; :: thesis: verum