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

( 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 :: thesis: for x being object holds

( ( x in A1 implies x in A2 ) & ( x in A2 implies x in A1 ) )

hence
p1 = p2
by A8, A10, TARSKI:2; :: thesis: verum( ( 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 )

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;thus ( x in A1 implies x in A2 ) :: thesis: ( x in A2 implies x in A1 )

proof

assume A13:
x in A2
; :: thesis: x in A1
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;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

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