let L be non trivial right_unital associative doubleLoopStr ; :: thesis: for a, b being Element of L st b is left_invertible & b is right_mult-cancelable & b * (/ b) = (/ b) * b holds
(a * b) / b = a
let a, b be Element of L; :: thesis: ( b is left_invertible & b is right_mult-cancelable & b * (/ b) = (/ b) * b implies (a * b) / b = a )
assume A1: ( b is left_invertible & b is right_mult-cancelable ) ; :: thesis: ( not b * (/ b) = (/ b) * b or (a * b) / b = a )
assume b * (/ b) = (/ b) * b ; :: thesis: (a * b) / b = a
then b * (/ b) = 1. L by A1, ALGSTR_0:def 30;
hence a = a * (b * (/ b))
.= (a * b) / b by GROUP_1:def 3 ;
:: thesis: verum