let R be commutative domRing-like Ring; :: thesis: for a, b, c being Element of R st a <> 0. R holds
( ( a * b = a * c implies b = c ) & ( b * a = c * a implies b = c ) )
let a, b, c be Element of R; :: thesis: ( a <> 0. R implies ( ( a * b = a * c implies b = c ) & ( b * a = c * a implies b = c ) ) )
assume A1: a <> 0. R ; :: thesis: ( ( a * b = a * c implies b = c ) & ( b * a = c * a implies b = c ) )
now :: thesis: ( a * b = a * c implies b = c )
assume a * b = a * c ; :: thesis: b = c
then 0. R = (a * b) + (- (a * c)) by RLVECT_1:def 10
.= (a * b) + (a * (- c)) by VECTSP_1:8
.= a * (b + (- c)) by VECTSP_1:def 2
.= a * (b - c) by RLVECT_1:def 11 ;
then b - c = 0. R by A1, VECTSP_2:def 1;
then c = (b - c) + c by RLVECT_1:4
.= (b + (- c)) + c by RLVECT_1:def 11
.= b + (c + (- c)) by RLVECT_1:def 3
.= b + (0. R) by RLVECT_1:def 10
.= b by RLVECT_1:4 ;
hence b = c ; :: thesis: verum
end;
hence ( ( a * b = a * c implies b = c ) & ( b * a = c * a implies b = c ) ) ; :: thesis: verum