theorem :: GAUSSINT:22

for K being Field
for K1 being Subfield of K
for x, y being Element of K
for x1, y1 being Element of K1 st x = x1 & y = y1 & y <> 0. K holds
x / y = x1 / y1