let X be Ordinal; :: thesis: for a, b being finite Subset of X st a <> b holds
(a,1) -bag <> (b,1) -bag
let a, b be finite Subset of X; :: thesis: ( a <> b implies (a,1) -bag <> (b,1) -bag )
assume A1: a <> b ; :: thesis: (a,1) -bag <> (b,1) -bag
assume A2: (a,1) -bag = (b,1) -bag ; :: thesis: contradiction

now :: thesis: for x being object holds
( x in a iff x in b )

let x be object ; :: thesis: ( x in a iff x in b )
( x in a iff ((b,1) -bag) . x = 1 ) by A2, UPROOTS:6, UPROOTS:7;
hence ( x in a iff x in b ) by UPROOTS:6, UPROOTS:7; :: thesis: verum

end;

hence contradiction by A1, TARSKI:2; :: thesis: verum