theorem qua20: :: FIELD_9:12

for R being Ring
for a, b, x being Element of R holds x * <%b,a%> = <%(x * b),(x * a)%>