let c, a, b be complex number ; :: thesis: ( c <> 0 implies a + b = ((a * c) + (b * c)) / c )
assume A1: c <> 0 ; :: thesis: a + b = ((a * c) + (b * c)) / c
hence a + b = ((a * c) / c) + b by Lm10
.= ((a * c) / c) + ((b * c) / c) by A1, Lm10
.= ((a * c) + (b * c)) / c by Th63 ;
:: thesis: verum