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 S_{1}[ 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 S_{1}[i]
;

consider i being Nat such that

A4: ( S_{1}[i] & ( for n being Nat st S_{1}[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 S_{2}[ Nat] means ( $1 < i implies (Partial_Sums (A -powers (1 / 2))) . $1 = (Partial_Sums (B -powers (1 / 2))) . $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: S_{2}[ 0 ]
by A14, A4, A5;

A18: for j being Nat holds S_{2}[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)

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

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 S

not for a being object holds

( a in X iff a in Y ) by A2, TARSKI:2;

then A3: ex i being Nat st S

consider i being Nat such that

A4: ( S

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 S

A9: now :: thesis: for j being Nat st S_{2}[j] holds

S_{2}[j + 1]

(Partial_Sums (A -powers (1 / 2))) . 0 = (A -powers (1 / 2)) . 0
by SERIES_1:def 1;S

let j be Nat; :: thesis: ( S_{2}[j] implies S_{2}[j + 1] )

assume A10: S_{2}[j]
; :: thesis: S_{2}[j + 1]

thus S_{2}[j + 1]
:: thesis: verum

end;assume A10: S

thus S

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

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

A18: for j being Nat holds S

A19: (Partial_Sums (A -powers (1 / 2))) . i = ((Partial_Sums (B -powers (1 / 2))) . i) + ((1 / 2) |^ i)

proof
end;

A21:
(Partial_Sums (A -powers (1 / 2))) . i < Sum (A -powers (1 / 2))
by Th26;per cases
( i = 0 or ex j being Nat st i = j + 1 )
by NAT_1:6;

end;

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

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