let L be non empty right_complementable almost_left_invertible add-associative right_zeroed left-distributive well-unital associative commutative doubleLoopStr ; :: thesis: 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; :: thesis: ( b <> 0. L implies eval (<%a,b%>,(- (a / b))) = 0. L )
assume b <> 0. L ; :: thesis: 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 ;
:: thesis: verum