theorem ch0a: :: FIELD_9:3

for F being Field
for a being Element of F
for b being non zero Element of F
for i being Integer st i '*' a <> 0. F & i '*' b <> 0. F holds
(i '*' a) * ((i '*' b) ") = a * (b ")