let c1, c2 be Complex; :: thesis: c1 + <%c2%> = <%(c1 + c2)%>
A1: ( dom <%(c1 + c2)%> = 1 & 1 = dom <%c2%> & dom <%c2%> = dom (c1 + <%c2%>) ) by VALUED_1:def 2, AFINSQ_1:def 4;
<%(c1 + c2)%> . 0 = c1 + (<%c2%> . 0)
.= (c1 + <%c2%>) . 0 by A1, AFINSQ_1:66, VALUED_1:def 2 ;
hence c1 + <%c2%> = <%(c1 + c2)%> by A1, AFINSQ_1:def 4; :: thesis: verum