let x, y be R_eal; :: thesis: ( y <> 0. implies for a, b being Real st x = a & y = b holds
x / y = a / b )
assume A1: y <> 0. ; :: 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 A2: ( x = a & y = b ) ; :: thesis: x / y = a / b
then consider a1, b1 being Real such that
A3: ( x = a1 & y = b1 & x / y = a1 / b1 ) by A1, Def2;
thus x / y = a / b by A2, A3; :: thesis: verum