let L be 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

1_ L = (1_1 (x2,L)) . (UnitBag x1) by A1, Th12

.= 0. L by A2, Th10, Th12 ;

hence contradiction ; :: thesis: verum

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

1_ L = (1_1 (x2,L)) . (UnitBag x1) by A1, Th12

.= 0. L by A2, Th10, Th12 ;

hence contradiction ; :: thesis: verum