theorem Th3: :: EC_PF_2:3

for K being Field
for a1, a2, a3, a4 being Element of K st a2 <> 0. K & a4 <> 0. K & a1 * (a2 ") = a3 * (a4 ") holds
a1 * a4 = a2 * a3