let a, b, c be real number ; :: thesis: ( a <> 0 & b <> 0 implies (a / b) * ((c / a) * b) = c )
assume that
A1: a <> 0 and
A2: b <> 0 ; :: thesis: (a / b) * ((c / a) * b) = c
(a / b) * ((c / a) * b) = ((a / b) * b) * (c / a)
.= a * (c / a) by A2, XCMPLX_1:88
.= c by A1, XCMPLX_1:88 ;
hence (a / b) * ((c / a) * b) = c ; :: thesis: verum