let x, y be Element of F_Rat; :: thesis: for x1, y1 being Rational st x1 = x & y1 = y & y <> 0. F_Rat holds
x / y = x1 / y1
let x1, y1 be Rational; :: thesis: ( x1 = x & y1 = y & y <> 0. F_Rat implies x / y = x1 / y1 )
assume A1: ( x1 = x & y1 = y & y <> 0. F_Rat ) ; :: thesis: x / y = x1 / y1
then y " = y1 " by Th15;
hence x / y = x1 / y1 by A1, BINOP_2:def 17; :: thesis: verum