let K be Field; :: thesis: 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
let K1 be Subfield of K; :: thesis: 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
let x, y be Element of K; :: thesis: for x1, y1 being Element of K1 st x = x1 & y = y1 & y <> 0. K holds
x / y = x1 / y1
let x1, y1 be Element of K1; :: thesis: ( x = x1 & y = y1 & y <> 0. K implies x / y = x1 / y1 )
set C = the carrier of K;
set C1 = the carrier of K1;
assume A1: ( x = x1 & y = y1 & y <> 0. K ) ; :: thesis: x / y = x1 / y1
then y " = y1 " by Th21;
hence x / y = x1 / y1 by A1, Th18; :: thesis: verum