let L be non empty non trivial right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr ; :: thesis: for X being non empty set
for x1, x2 being Element of X st 1_1 x1,L = 1_1 x2,L holds
x1 = x2
let X be non empty set ; :: thesis: for x1, x2 being Element of X st 1_1 x1,L = 1_1 x2,L holds
x1 = x2
let x1, x2 be Element of X; :: thesis: ( 1_1 x1,L = 1_1 x2,L implies x1 = x2 )
assume that
A1: 1_1 x1,L = 1_1 x2,L and
A2: x1 <> x2 ; :: thesis: contradiction
A3: UnitBag x1 <> UnitBag x2 by A2, Th10;
1_ L = (1_1 x2,L) . (UnitBag x1) by A1, Th12
.= 0. L by A3, Th12 ;
hence contradiction by POLYNOM1:27; :: thesis: verum