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 :: 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 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