let a, b, c be Complex; :: thesis: ( a <> 0 implies (((a ^2) * b) * c) / (a ^2) = b * c )
assume A1: a <> 0 ; :: thesis: (((a ^2) * b) * c) / (a ^2) = b * c
(((a ^2) * b) * c) / (a ^2) = (b * (a ^2)) * (c / (a ^2))
.= b * c by A1, XCMPLX_1:90 ;
hence (((a ^2) * b) * c) / (a ^2) = b * c ; :: thesis: verum