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:46, VALUED_1:def 5;

now

let x be set ; :: 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, Lm1
.= ((c multcomplex) * z) . x by A1, A2, FUNCT_1:22 ; :: thesis: verum

end;

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