let p1, p2 be FinSequence of i -tuples_on NAT; :: thesis: ( ex A being finite Subset of () st
( p1 = SgmX ((),A) & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) & ex A being finite Subset of () st
( p2 = SgmX ((),A) & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) implies p1 = p2 )

given A1 being finite Subset of () such that A8: p1 = SgmX ((),A1) and
A9: for p being Element of i -tuples_on NAT holds
( p in A1 iff Sum p = n ) ; :: thesis: ( for A being finite Subset of () holds
( not p2 = SgmX ((),A) or ex p being Element of i -tuples_on NAT st
( ( p in A implies Sum p = n ) implies ( Sum p = n & not p in A ) ) ) or p1 = p2 )

given A2 being finite Subset of () such that A10: p2 = SgmX ((),A2) and
A11: for p being Element of i -tuples_on NAT holds
( p in A2 iff Sum p = n ) ; :: thesis: p1 = p2
now :: thesis: for x being object holds
( ( x in A1 implies x in A2 ) & ( x in A2 implies x in A1 ) )
let x be object ; :: thesis: ( ( x in A1 implies x in A2 ) & ( x in A2 implies x in A1 ) )
thus ( x in A1 implies x in A2 ) :: thesis: ( x in A2 implies x in A1 )
proof
assume A12: x in A1 ; :: thesis: x in A2
then reconsider p = x as Element of i -tuples_on NAT ;
Sum p = n by ;
hence x in A2 by A11; :: thesis: verum
end;
assume A13: x in A2 ; :: thesis: x in A1
then reconsider p = x as Element of i -tuples_on NAT ;
Sum p = n by ;
hence x in A1 by A9; :: thesis: verum
end;
hence p1 = p2 by ; :: thesis: verum