let p1, p2 be FinSequence of i -tuples_on NAT ; :: thesis: ( ex A being finite Subset of (i -tuples_on NAT ) st
( p1 = SgmX (TuplesOrder i),A & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) & ex A being finite Subset of (i -tuples_on NAT ) st
( p2 = SgmX (TuplesOrder i),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 (i -tuples_on NAT ) such that A8: p1 = SgmX (TuplesOrder i),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 (i -tuples_on NAT ) holds
( not p2 = SgmX (TuplesOrder i),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 (i -tuples_on NAT ) such that A10: p2 = SgmX (TuplesOrder i),A2 and
A11: for p being Element of i -tuples_on NAT holds
( p in A2 iff Sum p = n ) ; :: thesis: p1 = p2

now

let x be set ; :: 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 A9, A12;
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 A11, A13;
hence x in A1 by A9; :: thesis: verum

end;

hence p1 = p2 by A8, A10, TARSKI:2; :: thesis: verum