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

(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 )

hence
contradiction
by A1, TARSKI:2; :: thesis: verum( 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;( 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