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

now :: thesis: for x being object st x in dom (abs z) holds
(abs z) . x = (abscomplex * z) . x

let x be object ; :: thesis: ( x in dom (abs z) implies (abs z) . x = (abscomplex * z) . x )
assume A2: x in dom (abs z) ; :: thesis: (abs z) . x = (abscomplex * z) . x
A3: z . x is Element of COMPLEX by XCMPLX_0:def 2;
thus (abs z) . x = |.(z . x).| by VALUED_1:18
.= abscomplex . (z . x) by A3, Def5
.= (abscomplex * z) . x by A1, A2, FUNCT_1:12 ; :: thesis: verum

end;

hence for b₁ being FinSequence of REAL holds
( b₁ = |.z.| iff b₁ = abscomplex * z ) by A1, FUNCT_1:2; :: thesis: verum