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

now

let z be Complex; :: thesis: (L1 - L2) /. z = (a1 - a2) * z
thus (L1 - L2) /. z = (L1 /. z) - (L2 /. z) by CFUNCT_1:76
.= (a1 * z) - (L2 /. z) by A3
.= (a1 * z) - (a2 * z) by A4
.= (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 ) by Def4; :: thesis: verum