consider a2 being Complex such that
A1: for z being Complex holds L2 /. z = a2 * z by Def4;
consider a1 being Complex such that
A2: for z being Complex holds L1 /. z = a1 * z by Def4;

now :: thesis: for z being Complex holds (L1 + L2) /. z = (a1 + a2) * z

let z be Complex; :: thesis: (L1 + L2) /. z = (a1 + a2) * z
z in COMPLEX by XCMPLX_0:def 2;
hence (L1 + L2) /. z = (L1 /. z) + (L2 /. z) by CFUNCT_1:64
.= (a1 * z) + (L2 /. z) by A2
.= (a1 * z) + (a2 * z) by A1
.= (a1 + a2) * z ;
:: thesis: verum

end;

hence for b₁ being PartFunc of COMPLEX,COMPLEX st b₁ = L1 + L2 holds
( b₁ is total & b₁ is linear ) ; :: thesis: verum