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

now

let x be set ; :: thesis: ( ( x in S1 implies x in S2 ) & ( x in S2 implies x in S1 ) )

hereby :: thesis: ( x in S2 implies x in S1 )

assume A5: x in S1 ; :: thesis: x in S2
then reconsider x9 = x as Element of Bags n ;
x9 divides b by A2, A5;
hence x in S2 by A4; :: thesis: verum

end;

assume A6: x in S2 ; :: thesis: x in S1
then reconsider x9 = x as Element of Bags n ;
x9 divides b by A4, A6;
hence x in S1 by A2; :: thesis: verum

end;

hence it1 = it2 by A1, A3, TARSKI:1; :: thesis: verum