theorem lemred1: :: FIELD_9:24

for F being Field
for b1, c1, b2, c2 being Element of F holds <%c1,b1%> *' <%c2,b2%> = <%(c1 * c2),((b1 * c2) + (b2 * c1)),(b1 * b2)%>