let x, y be R_eal; :: thesis: for a, b being Real st x = a & y = b holds
x / y = a / b
let a, b be Real; :: thesis: ( x = a & y = b implies x / y = a / b )
assume A1: ( x = a & y = b ) ; :: thesis: x / y = a / b
reconsider a = a, b = b as real number ;
consider c being complex number such that
A2: y = c and
A3: y " = c " by A1, XXREAL_3:def 6;
x / y = x * (y ")
.= a * (c ") by A1, A3, XXREAL_3:def 5
.= a / b by A1, A2 ;
hence x / y = a / b ; :: thesis: verum