let it1, it2 be FinSequence of Bags n; :: thesis: ( ex S being non empty finite Subset of (Bags n) st
( it1 = SgmX ((BagOrder n),S) & ( for p being bag of n holds
( p in S iff p divides b ) ) ) & ex S being non empty finite Subset of (Bags n) st
( it2 = SgmX ((BagOrder n),S) & ( for p being bag of n holds
( p in S iff p divides b ) ) ) implies it1 = it2 )
given S1 being non empty finite Subset of (Bags n) such that A1: it1 = SgmX ((BagOrder n),S1) and
A2: for p being bag of n holds
( p in S1 iff p divides b ) ; :: thesis: ( for S being non empty finite Subset of (Bags n) holds
( not it2 = SgmX ((BagOrder n),S) or ex p being bag of n st
( ( p in S implies p divides b ) implies ( p divides b & not p in S ) ) ) or it1 = it2 )
given S2 being non empty finite Subset of (Bags n) such that A3: it2 = SgmX ((BagOrder n),S2) and
A4: for p being bag of n holds
( p in S2 iff p divides b ) ; :: thesis: it1 = it2
for x being object holds
( x in S1 iff x in S2 ) by A2, A4;
hence it1 = it2 by A1, A3, TARSKI:2; :: thesis: verum