theorem Th05: :: BKMODEL3:5
for a, b, c being Complex st a <> 0 holds
((2 * ((a ^2) * b)) * c) / (a ^2) = (2 * b) * c