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
consider a being set such that
A3: ( ( a in X & not a in Y ) or ( a in Y & not a in X ) ) by A2, TARSKI:2;
defpred S₁[ Nat] means ( ( $1 in X & not $1 in Y ) or ( $1 in Y & not $1 in X ) );
ex i being Element of NAT st S₁[i] by A3;
then A4: ex i being Nat st S₁[i] ;
consider i being Nat such that
A5: ( S₁[i] & ( for n being Nat st S₁[n] holds
i <= n ) ) from NAT_1:sch 5(A4);
reconsider i = i as Element of NAT by ORDINAL1:def 13;
consider A, B being infinite Subset of NAT such that
A6: ( ( ( A = X & B = Y ) or ( A = Y & B = X ) ) & i in A & not i in B ) by A5;
A7: ( Sum (A -powers (1 / 2)) = ((Partial_Sums (A -powers (1 / 2))) . i) + (Sum ((A -powers (1 / 2)) ^\ (i + 1))) & Sum (B -powers (1 / 2)) = ((Partial_Sums (B -powers (1 / 2))) . i) + (Sum ((B -powers (1 / 2)) ^\ (i + 1))) ) by Th21, SERIES_1:18;
A8: (Partial_Sums (A -powers (1 / 2))) . i < Sum (A -powers (1 / 2)) by Th26;
A9: ( (A -powers (1 / 2)) . i = (1 / 2) |^ i & (B -powers (1 / 2)) . i = 0 ) by A6, Def5;
A10: Sum ((B -powers (1 / 2)) ^\ (i + 1)) <= (1 / 2) |^ i by Th25;
defpred S₂[ Element of NAT ] means ( $1 < i implies (Partial_Sums (A -powers (1 / 2))) . $1 = (Partial_Sums (B -powers (1 / 2))) . $1 );
A11: ( (Partial_Sums (A -powers (1 / 2))) . 0 = (A -powers (1 / 2)) . 0 & (Partial_Sums (B -powers (1 / 2))) . 0 = (B -powers (1 / 2)) . 0 ) by SERIES_1:def 1;
then ( ( ( 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 ) ) & ( ( 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 ) ) & ( 0 < i implies ( 0 in A iff 0 in B ) ) ) by A5, A6, Def5;
then A12: S₂[ 0 ] ;

A13: now

let j be Element of NAT ; :: thesis: ( S₂[j] implies S₂[j + 1] )
assume A14: S₂[j] ; :: thesis: S₂[j + 1]
thus S₂[j + 1] :: thesis: verum

proof

assume A15: j + 1 < i ; :: thesis: (Partial_Sums (A -powers (1 / 2))) . (j + 1) = (Partial_Sums (B -powers (1 / 2))) . (j + 1)
then A16: ( ( ( 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 ) ) & ( ( 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 ) ) & ( j + 1 in A implies j + 1 in B ) & ( j + 1 in B implies j + 1 in A ) ) by A5, A6, Def5;
thus (Partial_Sums (A -powers (1 / 2))) . (j + 1) = ((Partial_Sums (B -powers (1 / 2))) . j) + ((A -powers (1 / 2)) . (j + 1)) by A14, A15, NAT_1:13, SERIES_1:def 1
.= (Partial_Sums (B -powers (1 / 2))) . (j + 1) by A16, SERIES_1:def 1 ; :: thesis: verum

end;

end;

A17: for j being Element of NAT holds S₂[j] from NAT_1:sch 1(A12, A13);
(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 A9, A11; :: 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
A18: i = j + 1 ;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
j < i by A18, NAT_1:13;
then (Partial_Sums (A -powers (1 / 2))) . j = (Partial_Sums (B -powers (1 / 2))) . j by A17;
hence (Partial_Sums (A -powers (1 / 2))) . i = (((Partial_Sums (B -powers (1 / 2))) . j) + 0 ) + ((1 / 2) |^ i) by A9, A18, SERIES_1:def 1
.= ((Partial_Sums (B -powers (1 / 2))) . i) + ((1 / 2) |^ i) by A9, A18, SERIES_1:def 1 ;
:: thesis: verum

end;

end;

end;

hence contradiction by A1, A6, A7, A8, A10, XREAL_1:8; :: thesis: verum