let X be non empty set ; :: thesis: for x1, x2 being Element of X st UnitBag x1 = UnitBag x2 holds

x1 = x2

let x1, x2 be Element of X; :: thesis: ( UnitBag x1 = UnitBag x2 implies x1 = x2 )

assume that

A1: UnitBag x1 = UnitBag x2 and

A2: x1 <> x2 ; :: thesis: contradiction

1 = (UnitBag x2) . x1 by A1, Th9

.= 0 by A2, Th9 ;

hence contradiction ; :: thesis: verum

x1 = x2

let x1, x2 be Element of X; :: thesis: ( UnitBag x1 = UnitBag x2 implies x1 = x2 )

assume that

A1: UnitBag x1 = UnitBag x2 and

A2: x1 <> x2 ; :: thesis: contradiction

1 = (UnitBag x2) . x1 by A1, Th9

.= 0 by A2, Th9 ;

hence contradiction ; :: thesis: verum