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

now

let z be Complex; :: thesis: (a (#) L) /. z = (a * b) * z
thus (a (#) L) /. z = a * (L /. z) by CFUNCT_1:77
.= a * (b * z) by A1
.= (a * b) * z ; :: thesis: verum

end;

hence a (#) L is total linear PartFunc of COMPLEX , COMPLEX by Def4; :: thesis: verum