theorem Th6: :: COMPLFLD:6

for x1, y1 being Element of F_Complex
for x2, y2 being Complex st x1 = x2 & y1 = y2 & y1 <> 0. F_Complex holds
x1 / y1 = x2 / y2