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

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

hence
b = 0
by A2; :: thesis: verum
assume
c <> 0
; :: thesis: contradiction

then - (a ^2) = 1 by A3, XCMPLX_1:7;

hence contradiction ; :: thesis: verum

end;then - (a ^2) = 1 by A3, XCMPLX_1:7;

hence contradiction ; :: thesis: verum