let a, b be Real; :: thesis: ( a <> 0 implies a * (b / (2 * a)) = b / 2 )
assume A1: a <> 0 ; :: thesis: a * (b / (2 * a)) = b / 2
a * (b / (2 * a)) = (a * b) / (a * 2) by XCMPLX_1:74
.= ((a / a) * b) / 2 by XCMPLX_1:83
.= (1 * b) / 2 by A1, XCMPLX_1:60 ;
hence a * (b / (2 * a)) = b / 2 ; :: thesis: verum