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