consider b being Complex such that
A1: for z being Complex holds L /. z = b * z by Def4;

now :: thesis: for z being Complex holds (a (#) L) /. z = (a * b) * z

let z be Complex; :: thesis: (a (#) L) /. z = (a * b) * z
z in COMPLEX by XCMPLX_0:def 2;
hence (a (#) L) /. z = a * (L /. z) by CFUNCT_1:65
.= a * (b * z) by A1
.= (a * b) * z ;
:: thesis: verum

end;

hence for b₁ being PartFunc of COMPLEX,COMPLEX st b₁ = a (#) L holds
( b₁ is total & b₁ is linear ) ; :: thesis: verum