let L be non empty right_complementable almost_left_invertible add-associative right_zeroed left-distributive well-unital associative commutative doubleLoopStr ; for a, b, x being Element of L st b <> 0. L holds
eval (<%a,b%>,(- (a / b))) = 0. L
let a, b, x be Element of L; ( b <> 0. L implies eval (<%a,b%>,(- (a / b))) = 0. L )
assume
b <> 0. L
; eval (<%a,b%>,(- (a / b))) = 0. L
then A1:
b * (/ b) = 1. L
by VECTSP_1:def 10;
- (a / b) = (- a) / b
by VECTSP_1:9;
then b * (- (a / b)) =
(- a) * (1. L)
by A1, GROUP_1:def 3
.=
- a
;
hence eval (<%a,b%>,(- (a / b))) =
a + (- a)
by POLYNOM5:44
.=
0. L
by RLVECT_1:5
;
verum