let a, b, c, d be positive Real; :: thesis: ( a * b = c * d & a * c = b * d implies a = d )
assume ( a * b = c * d & a * c = b * d ) ; :: thesis: a = d
then (a * b) * (a * c) = (c * d) * (b * d) ;
then (a * a) * (b * c) = (d * d) * (b * c) ;
then a * a = d * d by XCMPLX_1:5;
then ( a >= d & d >= a ) by XREAL_1:96;
hence a = d by XXREAL_0:1; :: thesis: verum