let s be positive Nat; :: thesis:
set S = IncreasingSolutionsOfSumOfReciprocals s;
set S1 = IncreasingSolutionsOfSumOfReciprocals (s + 1);
assume s > 2 ; :: thesis:
then s >= 2 + 1 by NAT_1:13;

per cases by XXREAL_0:1;

suppose A1: s = 3 ; :: thesis:

then A2: card (IncreasingSolutionsOfSumOfReciprocals s) = 1 by Th123, CARD_1:30;
set f = <*2,3,7,42*>;
set g = <*2,3,8,24*>;
len <*2,3,7,42*> = 4 by CARD_1:def 7;
then ( 3 <= len <*2,3,7,42*> & <*2,3,7,42*> . 3 <> <*2,3,8,24*> . 3 ) ;
then A3: card {<*2,3,7,42*>,<*2,3,8,24*>} = 2 by CARD_2:57;
card {<*2,3,7,42*>,<*2,3,8,24*>} <= card (IncreasingSolutionsOfSumOfReciprocals (s + 1)) by A1, Th124, NAT_1:43;
hence card (IncreasingSolutionsOfSumOfReciprocals (s + 1)) > card (IncreasingSolutionsOfSumOfReciprocals s) by A2, A3, XXREAL_0:2; :: thesis:

end;

suppose A4: s > 3 ; :: thesis:

then A5: s - 1 > 3 - 1 by XREAL_1:9;
then reconsider t = s - 1 as positive Element of NAT by INT_1:3;
A6: 1 <= t + 1 by NAT_1:11;
consider f being t -element natural-valued increasing positive FinSequence such that
A7: f is with_sum_of_reciprocals_equal_1 by A5, Th121;
A8: len f = t by CARD_1:def 7;
A9: (Sierp162FS_2 f) . 2 = (2 * 1) + 1 by NUMBER14:21;
set X = (IncreasingSolutionsOfSumOfReciprocals s) \/ {f};
defpred S₁[ object , object ] means ( ( $1 = f implies $2 = Sierp162FS_2 f ) & ( $1 <> f implies ex h being complex-valued FinSequence st
( $1 = h & $2 = Sierp162FS h ) ) );
A10: for x being object st x in (IncreasingSolutionsOfSumOfReciprocals s) \/ {f} holds
ex y being object st
( y in IncreasingSolutionsOfSumOfReciprocals (s + 1) & S₁[x,y] )

let x be object ; :: thesis:
assume x in (IncreasingSolutionsOfSumOfReciprocals s) \/ {f} ; :: thesis:

per cases by ZFMISC_1:136;

suppose x in IncreasingSolutionsOfSumOfReciprocals s ; :: thesis:

then consider X being t + 1 -element natural-valued increasing positive FinSequence such that
A11: x = X and
A12: X is with_sum_of_reciprocals_equal_1 ;
take q = Sierp162FS X; :: thesis:
A13: q is increasing by A4, A12, Th114, XXREAL_0:2;
A14: q is with_sum_of_reciprocals_equal_1 by A12, Th116;
len X = t + 1 by CARD_1:def 7;
hence ( q in IncreasingSolutionsOfSumOfReciprocals (s + 1) & S₁[x,q] ) by A8, A11, A13, A14; :: thesis:

end;

suppose A15: x = f ; :: thesis:

take q = Sierp162FS_2 f; :: thesis:
A16: q is increasing by Th115;
q is with_sum_of_reciprocals_equal_1 by A7, Th117;
hence ( q in IncreasingSolutionsOfSumOfReciprocals (s + 1) & S₁[x,q] ) by A15, A16; :: thesis:

end;

end;

end;

consider F being Function such that
A17: dom F = (IncreasingSolutionsOfSumOfReciprocals s) \/ {f} and
A18: rng F c= IncreasingSolutionsOfSumOfReciprocals (s + 1) and
A19: for x being object st x in (IncreasingSolutionsOfSumOfReciprocals s) \/ {f} holds
S₁[x,F . x] from FUNCT_1:sch 6(A10);
F is one-to-one

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A20: x1 in dom F and
A21: x2 in dom F and
A22: F . x1 = F . x2 ; :: thesis:
A23: S₁[x1,F . x1] by A17, A19, A20;
A24: S₁[x2,F . x2] by A17, A19, A21;

per cases by A17, A20, ZFMISC_1:136;

suppose x1 in IncreasingSolutionsOfSumOfReciprocals s ; :: thesis:

then consider F1 being t + 1 -element natural-valued increasing positive FinSequence such that
A25: x1 = F1 and
F1 is with_sum_of_reciprocals_equal_1 ;
A26: len F1 = t + 1 by CARD_1:def 7;

per cases by A17, A21, ZFMISC_1:136;

suppose x2 in IncreasingSolutionsOfSumOfReciprocals s ; :: thesis:

then consider F2 being t + 1 -element natural-valued increasing positive FinSequence such that
A27: x2 = F2 and
F2 is with_sum_of_reciprocals_equal_1 ;
len F2 = t + 1 by CARD_1:def 7;
then 2 (#) F1 = 2 (#) F2 by A8, A22, A23, A24, A25, A26, A27, FINSEQ_1:33;
hence x1 = x2 by A25, A27, Th49; :: thesis:

end;

suppose A28: x2 = f ; :: thesis:

consider h being complex-valued FinSequence such that
A29: x1 = h and
F . x1 = Sierp162FS h by A8, A23, A25, A26;
A30: len h = t + 1 by A25, A29, CARD_1:def 7;
dom (2 (#) h) = dom h by VALUED_1:def 5;
then (Sierp162FS h) . (1 + 1) = (2 (#) h) . 1 by A6, A30, FINSEQ_3:25, FINSEQ_3:103
.= 2 * (h . 1) by VALUED_1:6 ;
hence x1 = x2 by A9, A22, A23, A24, A25, A28, A29; :: thesis:

end;

end;

end;

suppose A31: x1 = f ; :: thesis:

per cases by A17, A21, ZFMISC_1:136;

suppose x2 in IncreasingSolutionsOfSumOfReciprocals s ; :: thesis:

then consider F2 being t + 1 -element natural-valued increasing positive FinSequence such that
A32: x2 = F2 and
F2 is with_sum_of_reciprocals_equal_1 ;
len F2 = t + 1 by CARD_1:def 7;
then consider h being complex-valued FinSequence such that
A33: x2 = h and
F . x2 = Sierp162FS h by A8, A24, A32;
A34: len h = t + 1 by A32, A33, CARD_1:def 7;
dom (2 (#) h) = dom h by VALUED_1:def 5;
then (Sierp162FS h) . (1 + 1) = (2 (#) h) . 1 by A6, A34, FINSEQ_3:25, FINSEQ_3:103
.= 2 * (h . 1) by VALUED_1:6 ;
hence x1 = x2 by A9, A22, A23, A24, A31, A32, A33; :: thesis:

end;

suppose x2 = f ; :: thesis:

hence x1 = x2 by A31; :: thesis:

end;

end;

end;

end;

end;

then Segm (card ((IncreasingSolutionsOfSumOfReciprocals s) \/ {f})) c= Segm (card (IncreasingSolutionsOfSumOfReciprocals (s + 1))) by A17, A18, CARD_1:10;
then A35: card ((IncreasingSolutionsOfSumOfReciprocals s) \/ {f}) <= card (IncreasingSolutionsOfSumOfReciprocals (s + 1)) by NAT_1:39;
IncreasingSolutionsOfSumOfReciprocals s misses {f}

assume IncreasingSolutionsOfSumOfReciprocals s meets {f} ; :: thesis:
then consider x being object such that
A36: x in IncreasingSolutionsOfSumOfReciprocals s and
A37: x in {f} by XBOOLE_0:3;
x = f by A37, TARSKI:def 1;
then consider F1 being t + 1 -element natural-valued increasing positive FinSequence such that
A38: f = F1 and
F1 is with_sum_of_reciprocals_equal_1 by A36;
len F1 = t + 1 by CARD_1:def 7;
hence contradiction by A8, A38; :: thesis:

end;

then card ((IncreasingSolutionsOfSumOfReciprocals s) \/ {f}) = (card (IncreasingSolutionsOfSumOfReciprocals s)) + (card {f}) by CARD_2:40
.= (card (IncreasingSolutionsOfSumOfReciprocals s)) + 1 by CARD_1:30 ;
hence card (IncreasingSolutionsOfSumOfReciprocals s) < card (IncreasingSolutionsOfSumOfReciprocals (s + 1)) by A35, NAT_1:13; :: thesis:

end;

end;