theorem :: AFINSQ_1:90

for x, y being object holds <%x%> +~ (x,y) = <%y%>