let s be Nat; :: thesis: for w being Rational holds { f where f is s -element natural-valued positive-yielding FinSequence : Sum (f ") = w } is finite
let w be Rational; :: thesis: { f where f is s -element natural-valued positive-yielding FinSequence : Sum (f ") = w } is finite
set A = { f where f is s -element natural-valued positive FinSequence : Sum (f ") = w } ;
set I = { f where f is s -element natural-valued non-decreasing positive FinSequence : Sum (f ") = w } ;
{ f where f is s -element natural-valued non-decreasing positive FinSequence : Sum (f ") = w } is functional

proof

let x be object ; :: according to FUNCT_1:def 13 :: thesis: ( not x in { f where f is s -element natural-valued non-decreasing positive FinSequence : Sum (f ") = w } or x is set )
assume x in { f where f is s -element natural-valued non-decreasing positive FinSequence : Sum (f ") = w } ; :: thesis: x is set
then ex f being s -element natural-valued non-decreasing positive FinSequence st
( x = f & Sum (f ") = w ) ;
hence x is set ; :: thesis: verum

end;

then reconsider Ip = { f where f is s -element natural-valued non-decreasing positive FinSequence : Sum (f ") = w } as functional set ;
A1: { f where f is s -element natural-valued non-decreasing positive FinSequence : Sum (f ") = w } is finite by Th111;
for X being set st X in Permutations Ip holds
X is finite

proof

let X be set ; :: thesis: ( X in Permutations Ip implies X is finite )
assume X in Permutations Ip ; :: thesis: X is finite
then consider E being Element of Ip such that
A2: X = Permutations E and
A3: E in Ip ;
ex f being s -element natural-valued non-decreasing positive FinSequence st
( E = f & Sum (f ") = w ) by A3;
hence X is finite by A2; :: thesis: verum

end;

then A4: union (Permutations Ip) is finite by A1, FINSET_1:7;
deffunc H₂( natural-valued FinSequence) -> FinSequence of REAL = sort_a $1;
{ f where f is s -element natural-valued positive FinSequence : Sum (f ") = w } c= union (Permutations Ip)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { f where f is s -element natural-valued positive FinSequence : Sum (f ") = w } or a in union (Permutations Ip) )
assume a in { f where f is s -element natural-valued positive FinSequence : Sum (f ") = w } ; :: thesis: a in union (Permutations Ip)
then consider f being s -element natural-valued positive FinSequence such that
A5: a = f and
A6: Sum (f ") = w ;
A7: f,H₂(f) are_fiberwise_equipotent by RFINSEQ2:def 6;
then consider P being Permutation of (dom H₂(f)) such that
A8: f = H₂(f) * P by RFINSEQ:4;
Sum (H₂(f) ") = Sum (f ") by A7, Th109, RFINSEQ:9;
then A9: H₂(f) in Ip by A6;
A10: a in Permutations H₂(f) by A5, A8;
Permutations H₂(f) in Permutations Ip by A9;
hence a in union (Permutations Ip) by A10, TARSKI:def 4; :: thesis: verum

end;

hence { f where f is s -element natural-valued positive-yielding FinSequence : Sum (f ") = w } is finite by A4; :: thesis: verum