let n be Nat; :: thesis: for f1, f2 being one-to-one natural-valued FinSequence st n > 1 & ((n |^ f1) . 1) + (((n |^ f1),2) +...) = ((n |^ f2) . 1) + (((n |^ f2),2) +...) holds
rng f1 = rng f2
let f1, f2 be one-to-one natural-valued FinSequence; :: thesis: ( n > 1 & ((n |^ f1) . 1) + (((n |^ f1),2) +...) = ((n |^ f2) . 1) + (((n |^ f2),2) +...) implies rng f1 = rng f2 )
assume A1: ( n > 1 & ((n |^ f1) . 1) + (((n |^ f1),2) +...) = ((n |^ f2) . 1) + (((n |^ f2),2) +...) ) ; :: thesis: rng f1 = rng f2
A2: ( rng f1 c= NAT & rng f2 c= NAT ) by VALUED_0:def 6;
then reconsider F1 = f1, F2 = f2 as FinSequence of REAL by FINSEQ_1:def 4;
set s1 = sort_a F1;
set s2 = sort_a F2;
A3: ( F1, sort_a F1 are_fiberwise_equipotent & F2, sort_a F2 are_fiberwise_equipotent ) by RFINSEQ2:def 6;
A4: rng (sort_a F1) = rng f1 by RFINSEQ2:def 6, CLASSES1:75;
then A5: sort_a F1 is natural-valued by A2, VALUED_0:def 6;
n |^ F1,n |^ (sort_a F1) are_fiberwise_equipotent by A3, A1, A5, Th29;
then A8: Sum (n |^ F1) = Sum (n |^ (sort_a F1)) by RFINSEQ:9;
A9: rng (sort_a F2) = rng f2 by RFINSEQ2:def 6, CLASSES1:75;
then A10: sort_a F2 is natural-valued by A2, VALUED_0:def 6;
A12: sort_a F2 is natural-valued by A9, A2, VALUED_0:def 6;
n |^ F2,n |^ (sort_a F2) are_fiberwise_equipotent by A10, A3, A1, Th29;
then A14: Sum (n |^ F2) = Sum (n |^ (sort_a F2)) by RFINSEQ:9;
A15: for e1, e2 being ExtReal st e1 in dom (sort_a F1) & e2 in dom (sort_a F1) & e1 < e2 holds
(sort_a F1) . e1 < (sort_a F1) . e2

proof

let e1, e2 be ExtReal; :: thesis: ( e1 in dom (sort_a F1) & e2 in dom (sort_a F1) & e1 < e2 implies (sort_a F1) . e1 < (sort_a F1) . e2 )
assume A16: ( e1 in dom (sort_a F1) & e2 in dom (sort_a F1) & e1 < e2 ) ; :: thesis: (sort_a F1) . e1 < (sort_a F1) . e2
then A17: (sort_a F1) . e1 <= (sort_a F1) . e2 by INTEGRA2:2;
assume A18: (sort_a F1) . e1 >= (sort_a F1) . e2 ; :: thesis: contradiction
consider H being Function such that
A19: ( dom H = dom (sort_a F1) & rng H = dom F1 & H is one-to-one & sort_a F1 = F1 * H ) by A3, CLASSES1:77;
sort_a F1 is one-to-one by A19;
hence contradiction by A18, A17, XXREAL_0:1, A16; :: thesis: verum

end;

for e1, e2 being ExtReal st e1 in dom (sort_a F2) & e2 in dom (sort_a F2) & e1 < e2 holds
(sort_a F2) . e1 < (sort_a F2) . e2

proof

let e1, e2 be ExtReal; :: thesis: ( e1 in dom (sort_a F2) & e2 in dom (sort_a F2) & e1 < e2 implies (sort_a F2) . e1 < (sort_a F2) . e2 )
assume A20: ( e1 in dom (sort_a F2) & e2 in dom (sort_a F2) & e1 < e2 ) ; :: thesis: (sort_a F2) . e1 < (sort_a F2) . e2
then A21: (sort_a F2) . e1 <= (sort_a F2) . e2 by INTEGRA2:2;
assume A22: (sort_a F2) . e1 >= (sort_a F2) . e2 ; :: thesis: contradiction
consider H being Function such that
A23: ( dom H = dom (sort_a F2) & rng H = dom F2 & H is one-to-one & sort_a F2 = F2 * H ) by A3, CLASSES1:77;
sort_a F2 is one-to-one by A23;
hence contradiction by A22, A21, XXREAL_0:1, A20; :: thesis: verum

end;

then A24: sort_a F2 is increasing by VALUED_0:def 13;
A25: Sum (n |^ (sort_a F1)) = ((n |^ (sort_a F1)) . 1) + (((n |^ (sort_a F1)),2) +...) by Th22;
Sum (n |^ f1) = ((n |^ f1) . 1) + (((n |^ f1),2) +...) by Th22;
then Sum (n |^ (sort_a F1)) = Sum (n |^ (sort_a F2)) by Th22, A1, A8, A14;
then ( ((n |^ (sort_a F1)) . 1) + (((n |^ (sort_a F1)),2) +...) = ((n |^ (sort_a F2)) . 1) + (((n |^ (sort_a F2)),2) +...) & sort_a F1 is increasing & sort_a F1 is natural-valued ) by A15, VALUED_0:def 13, A25, Th22, A4, A2, VALUED_0:def 6;
hence rng f1 = rng f2 by A1, A12, A24, Th27, A9, A4; :: thesis: verum