let s be Nat; :: thesis: ( s > 2 implies ex f being s -element natural-valued increasing positive-yielding FinSequence st f is with_sum_of_reciprocals_equal_1 )
assume s > 2 ; :: thesis: ex f being s -element natural-valued increasing positive-yielding FinSequence st f is with_sum_of_reciprocals_equal_1
then A1: s >= 2 + 1 by NAT_1:13;
defpred S₁[ Nat] means ex f being $1 -element natural-valued increasing positive FinSequence st f is with_sum_of_reciprocals_equal_1 ;
A2: S₁[3] by Th118;
A3: for j being Nat st 3 <= j & S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( 3 <= j & S₁[j] implies S₁[j + 1] )
assume A4: 3 <= j ; :: thesis: ( not S₁[j] or S₁[j + 1] )
given f being j -element natural-valued increasing positive FinSequence such that A5: f is with_sum_of_reciprocals_equal_1 ; :: thesis: S₁[j + 1]
set g = Sierp162FS f;
reconsider g = Sierp162FS f as j + 1 -element natural-valued increasing positive FinSequence by A4, A5, Th114, XXREAL_0:2;
take g ; :: thesis: g is with_sum_of_reciprocals_equal_1
thus g is with_sum_of_reciprocals_equal_1 by A5, Th116; :: thesis: verum

end;

for i being Nat st 3 <= i holds
S₁[i] from NAT_1:sch 8(A2, A3);
hence ex f being s -element natural-valued increasing positive-yielding FinSequence st f is with_sum_of_reciprocals_equal_1 by A1; :: thesis: verum