set r = 1 / 2;
let X, Y be infinite Subset of NAT; :: thesis: ( Sum (X -powers (1 / 2)) = Sum (Y -powers (1 / 2)) implies X = Y )
assume that
A1: Sum (X -powers (1 / 2)) = Sum (Y -powers (1 / 2)) and
A2: X <> Y ; :: thesis: contradiction
defpred S1[ Nat] means ( ( $1 in X & not $1 in Y ) or ( $1 in Y & not $1 in X ) );
not for a being object holds
( a in X iff a in Y ) by A2, TARSKI:2;
then A3: ex i being Nat st S1[i] ;
consider i being Nat such that
A4: ( S1[i] & ( for n being Nat st S1[n] holds
i <= n ) ) from NAT_1:sch 5(A3);
 reconsider i = i as Element of NAT by ORDINAL1:def 12;
consider A, B being infinite Subset of NAT such that
A5: ( ( A = X & B = Y ) or ( A = Y & B = X ) ) and
A6: i in A and
A7: not i in B by A4;
A8: (A -powers (1 / 2)) . i = (1 / 2) |^ i by A6, Def5;
defpred S2[ Nat] means ( $1 < i implies (Partial_Sums (A -powers (1 / 2))) . $1 = (Partial_Sums (B -powers (1 / 2))) . $1 );
A9: now :: thesis: for j being Nat st S2[j] holds
S2[j + 1]
let j be Nat; :: thesis: ( S2[j] implies S2[j + 1] )
assume A10: S2[j] ; :: thesis: S2[j + 1]
thus S2[j + 1] :: thesis: verum
proof
A11: ( ( j + 1 in B & (B -powers (1 / 2)) . (j + 1) = (1 / 2) |^ (j + 1) ) or ( not j + 1 in B & (B -powers (1 / 2)) . (j + 1) = 0 ) ) by Def5;
A12: ( ( j + 1 in A & (A -powers (1 / 2)) . (j + 1) = (1 / 2) |^ (j + 1) ) or ( not j + 1 in A & (A -powers (1 / 2)) . (j + 1) = 0 ) ) by Def5;
assume A13: j + 1 < i ; :: thesis: (Partial_Sums (A -powers (1 / 2))) . (j + 1) = (Partial_Sums (B -powers (1 / 2))) . (j + 1)
hence (Partial_Sums (A -powers (1 / 2))) . (j + 1) = ((Partial_Sums (B -powers (1 / 2))) . j) + ((A -powers (1 / 2)) . (j + 1)) by A10, NAT_1:13, SERIES_1:def 1
.= (Partial_Sums (B -powers (1 / 2))) . (j + 1) by A12, A11, A13, A4, A5, SERIES_1:def 1 ;
:: thesis: verum
end;
end;
(Partial_Sums (A -powers (1 / 2))) . 0 = (A -powers (1 / 2)) . 0 by SERIES_1:def 1;
then A14: ( ( 0 in A & (Partial_Sums (A -powers (1 / 2))) . 0 = (1 / 2) |^ 0 ) or ( not 0 in A & (Partial_Sums (A -powers (1 / 2))) . 0 = 0 ) ) by Def5;
A15: (B -powers (1 / 2)) . i = 0 by A7, Def5;
A16: (Partial_Sums (B -powers (1 / 2))) . 0 = (B -powers (1 / 2)) . 0 by SERIES_1:def 1;
then ( ( 0 in B & (Partial_Sums (B -powers (1 / 2))) . 0 = (1 / 2) |^ 0 ) or ( not 0 in B & (Partial_Sums (B -powers (1 / 2))) . 0 = 0 ) ) by Def5;
then A17: S2[ 0 ] by A14, A4, A5;
A18: for j being Nat holds S2[j] from NAT_1:sch 2(A17, A9);
 A19: (Partial_Sums (A -powers (1 / 2))) . i = ((Partial_Sums (B -powers (1 / 2))) . i) + ((1 / 2) |^ i)
proof
per cases ( i = 0 or ex j being Nat st i = j + 1 ) by NAT_1:6;
suppose i = 0 ; :: thesis: (Partial_Sums (A -powers (1 / 2))) . i = ((Partial_Sums (B -powers (1 / 2))) . i) + ((1 / 2) |^ i)
hence (Partial_Sums (A -powers (1 / 2))) . i = ((Partial_Sums (B -powers (1 / 2))) . i) + ((1 / 2) |^ i) by A8, A15, A16, SERIES_1:def 1; :: thesis: verum
end;
suppose ex j being Nat st i = j + 1 ; :: thesis: (Partial_Sums (A -powers (1 / 2))) . i = ((Partial_Sums (B -powers (1 / 2))) . i) + ((1 / 2) |^ i)
then consider j being Nat such that
A20: i = j + 1 ;
reconsider j = j as Element of NAT by ORDINAL1:def 12;
j < i by A20, NAT_1:13;
then (Partial_Sums (A -powers (1 / 2))) . j = (Partial_Sums (B -powers (1 / 2))) . j by A18;
hence (Partial_Sums (A -powers (1 / 2))) . i = (((Partial_Sums (B -powers (1 / 2))) . j) + 0) + ((1 / 2) |^ i) by A8, A20, SERIES_1:def 1
.= ((Partial_Sums (B -powers (1 / 2))) . i) + ((1 / 2) |^ i) by A15, A20, SERIES_1:def 1 ;
:: thesis: verum
end;
end;
end;
A21: (Partial_Sums (A -powers (1 / 2))) . i < Sum (A -powers (1 / 2)) by Th26;
A22: Sum ((B -powers (1 / 2)) ^\ (i + 1)) <= (1 / 2) |^ i by Th25;
Sum (B -powers (1 / 2)) = ((Partial_Sums (B -powers (1 / 2))) . i) + (Sum ((B -powers (1 / 2)) ^\ (i + 1))) by Th21, SERIES_1:15;
hence contradiction by A19, A1, A5, A21, A22, XREAL_1:6; :: thesis: verum