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