let a, b, c be Real; :: thesis: ( a * (- b) = c & a * c = b implies ( c = 0 & b = 0 ) )
assume that
A1: a * (- b) = c and
A2: a * c = b ; :: thesis: ( c = 0 & b = 0 )
a * (- (a * c)) = c by A1, A2;
then A3: (- (a * a)) * c = c ;
thus c = 0 :: thesis: b = 0
proof
assume c <> 0 ; :: thesis: contradiction
then - (a ^2) = 1 by A3, XCMPLX_1:7;
hence contradiction ; :: thesis: verum
end;
hence b = 0 by A2; :: thesis: verum