let n be Nat; :: thesis: for f1, f2 being natural-valued increasing FinSequence st n > 1 & ((n |^ f1) . 1) + (((n |^ f1),2) +...) = ((n |^ f2) . 1) + (((n |^ f2),2) +...) holds
f1 = f2
A1: for f being natural-valued FinSequence st n > 1 & Sum (n |^ f) <= 0 holds
f = {}

proof

let f be natural-valued FinSequence; :: thesis: ( n > 1 & Sum (n |^ f) <= 0 implies f = {} )
assume A2: ( n > 1 & Sum (n |^ f) <= 0 ) ; :: thesis: f = {}
assume f <> {} ; :: thesis: contradiction
then consider x being object such that
A3: x in dom f by XBOOLE_0:def 1;
reconsider x = x as Nat by A3;
A4: for i being Nat st i in dom (n |^ f) holds
0 <= (n |^ f) . i ;
dom (n |^ f) = dom f by Def4;
then A5: 0 >= (n |^ f) . x by A4, A2, RVSUM_1:85, A3;
n to_power (f . x) > 0 by A2, NEWTON:83;
hence contradiction by A5, A3, Def4; :: thesis: verum

end;

defpred S₁[ Nat] means for f1, f2 being natural-valued increasing FinSequence st n > 1 & Sum (n |^ f1) <= $1 & Sum (n |^ f1) = Sum (n |^ f2) holds
f1 = f2;
A6: S₁[ 0 ]

proof

let f1, f2 be natural-valued increasing FinSequence; :: thesis: ( n > 1 & Sum (n |^ f1) <= 0 & Sum (n |^ f1) = Sum (n |^ f2) implies f1 = f2 )
assume A7: ( n > 1 & Sum (n |^ f1) <= 0 & Sum (n |^ f1) = Sum (n |^ f2) ) ; :: thesis: f1 = f2
f1 = {} by A7, A1;
hence f1 = f2 by A7, A1; :: thesis: verum

end;

A8: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A9: S₁[i] ; :: thesis: S₁[i + 1]
set i1 = i + 1;
let f1, f2 be natural-valued increasing FinSequence; :: thesis: ( n > 1 & Sum (n |^ f1) <= i + 1 & Sum (n |^ f1) = Sum (n |^ f2) implies f1 = f2 )
assume A10: ( n > 1 & Sum (n |^ f1) <= i + 1 & Sum (n |^ f1) = Sum (n |^ f2) ) ; :: thesis: f1 = f2

per cases ( Sum (n |^ f1) <= i or Sum (n |^ f1) = i + 1 ) by A10, NAT_1:8;

suppose Sum (n |^ f1) <= i ; :: thesis: f1 = f2

hence f1 = f2 by A10, A9; :: thesis: verum

end;

suppose A12: Sum (n |^ f1) = i + 1 ; :: thesis: f1 = f2

set l1 = len f1;
set l2 = len f2;
A13: f1 <> {} by A12, RVSUM_1:72;
A14: f2 <> {} by A10, A12, RVSUM_1:72;
A15: f1 . (len f1) <= f2 . (len f2) by Lm6, A10, A12;
A16: f1 . (len f1) >= f2 . (len f2) by Lm6, A10, A12;
then A17: f1 . (len f1) = f2 . (len f2) by A15, XXREAL_0:1;
reconsider L1 = (len f1) - 1, L2 = (len f2) - 1 as Nat by A14, A13;
reconsider F1 = f1 | L1, F2 = f2 | L2 as natural-valued increasing FinSequence ;
A18: n |^ (f2 . (len f2)) = n |^ (f1 . (len f1)) by A16, A15, XXREAL_0:1;
A19: ( len f1 = L1 + 1 & len f2 = L2 + 1 ) ;
then A20: ( Sum (n |^ f1) = (Sum (n |^ F1)) + (n |^ (f1 . (len f1))) & Sum (n |^ f2) = (Sum (n |^ F2)) + (n |^ (f2 . (len f2))) ) by Lm5;
n |^ (f1 . (len f1)) > 0 by PREPOWER:6, A10;
then (Sum (n |^ F1)) + 0 < Sum (n |^ f1) by A20, XREAL_1:8;
then A22: Sum (n |^ F1) <= i by A12, NAT_1:13;
( f1 = F1 ^ <*(f1 . (len f1))*> & f2 = F2 ^ <*(f2 . (len f2))*> ) by A19, FINSEQ_3:55;
hence f1 = f2 by A17, A22, A10, A20, A18, A9; :: thesis: verum

end;

end;

end;

A23: for i being Nat holds S₁[i] from NAT_1:sch 2(A6, A8);
let f1, f2 be natural-valued increasing FinSequence; :: thesis: ( n > 1 & ((n |^ f1) . 1) + (((n |^ f1),2) +...) = ((n |^ f2) . 1) + (((n |^ f2),2) +...) implies f1 = f2 )
A24: ((n |^ f1) . 1) + (((n |^ f1),2) +...) = Sum (n |^ f1) by Th22;
((n |^ f2) . 1) + (((n |^ f2),2) +...) = Sum (n |^ f2) by Th22;
hence ( n > 1 & ((n |^ f1) . 1) + (((n |^ f1),2) +...) = ((n |^ f2) . 1) + (((n |^ f2),2) +...) implies f1 = f2 ) by A23, A24; :: thesis: verum