theorem Th1: :: NIVEN:1

for a, b, c, d being Complex st b <> 0 & a / b = c / d holds
a = (b * c) / d