defpred S₁[ Nat] means ex f being non-empty $1 + 1 -element natural-valued FinSequence st f is a_solution_of_Sierp168 ;
A1: S₁[1] by Th67;
A2: for s being non zero Nat st S₁[s] holds
S₁[s + 1]

proof

let s be non zero Nat; :: thesis: ( S₁[s] implies S₁[s + 1] )
given T being non-empty s + 1 -element natural-valued FinSequence such that A3: T is a_solution_of_Sierp168 ; :: thesis: S₁[s + 1]
take X = SierpProblem168FS T; :: thesis: X is a_solution_of_Sierp168
A4: 12 (#) (T | (s - 1)) = (12 (#) T) | (s - 1) by Th56;
A5: len <*(15 * (T . s)),(20 * (T . s))*> = 2 by FINSEQ_1:44;
A6: len (12 (#) T) = len T by COMPLSP2:3;
A7: len T = s + 1 by CARD_1:def 7;
then A8: len (12 (#) (T | (s - 1))) = s - 1 by A4, A6, FINSEQ_1:59, XREAL_1:6;
A9: len ((12 (#) (T | (s - 1))) ^ <*(15 * (T . s)),(20 * (T . s))*>) = (len (12 (#) (T | (s - 1)))) + (len <*(15 * (T . s)),(20 * (T . s))*>) by FINSEQ_1:22
.= s + 1 by A5, A8 ;
A10: len <*(15 * (T . s)),(20 * (T . s)),(12 * (T . (s + 1)))*> = 3 by FINSEQ_1:45;
( ((s - 1) + 1) + 0 <= s + 2 & s + 2 <= (s - 1) + 3 ) by XREAL_1:6;
then A11: ((12 (#) (T | (s - 1))) ^ <*(15 * (T . s)),(20 * (T . s)),(12 * (T . (s + 1)))*>) . (s + 2) = <*(15 * (T . s)),(20 * (T . s)),(12 * (T . (s + 1)))*> . ((s + 2) - (s - 1)) by A8, A10, FINSEQ_1:23;
A12: ((12 ") (#) (T ")) ^2 = ((12 ") ^2) (#) ((T ") ^2) by BORSUK_7:18;
A13: ((T ") | s) ^2 = ((T ") ^2) | s by Th62;
A14: ((T | s) ") ^2 = ((T ") | s) ^2 by Th61;
((T ") ^2) . s = ((T ") . s) ^2 by VALUED_1:11;
then A15: ((T ") ^2) . s = ((T . s) ") ^2 by VALUED_1:10;
A16: 0 + 1 <= s by NAT_1:13;
s <= s + 1 by NAT_1:11;
then s in dom T by A7, A16, FINSEQ_3:25;
then A17: T . s <> 0 ;
then A18: (1 / ((15 * (T . s)) ^2)) + (1 / ((20 * (T . s)) ^2)) = ((1 * ((20 ^2) * ((T . s) ^2))) + (1 * ((15 ^2) * ((T . s) ^2)))) / (((15 ^2) * ((T . s) ^2)) * ((20 ^2) * ((T . s) ^2))) by XCMPLX_1:116
.= (625 * ((T . s) ^2)) / (((225 * ((T . s) ^2)) * 400) * ((T . s) ^2))
.= (1 * 625) / (((12 ^2) * ((T . s) ^2)) * 625) by A17, XCMPLX_1:91
.= 1 / ((12 * (T . s)) ^2) by XCMPLX_1:91 ;
((12 (#) T) | (s - 1)) " = ((12 (#) T) ") | (s - 1) by Th61;
then A19: Sum ((((12 (#) T) | (s - 1)) ") ^2) = Sum ((((12 (#) T) ") ^2) | (s - 1)) by Th62;

now :: thesis: for c being Complex holds ((c * (T . s)) ") ^2 = (1 * 1) / ((c * (T . s)) ^2)

let c be Complex; :: thesis: ((c * (T . s)) ") ^2 = (1 * 1) / ((c * (T . s)) ^2)
thus ((c * (T . s)) ") ^2 = (1 / (c * (T . s))) ^2
.= (1 * 1) / ((c * (T . s)) ^2) by XCMPLX_1:76 ; :: thesis: verum

end;

then A20: ( ((15 * (T . s)) ") ^2 = 1 / ((15 * (T . s)) ^2) & ((20 * (T . s)) ") ^2 = 1 / ((20 * (T . s)) ^2) ) ;
(<*(15 * (T . s)),(20 * (T . s))*> ") ^2 = <*((15 * (T . s)) "),((20 * (T . s)) ")*> ^2 by Th64
.= <*(1 / ((15 * (T . s)) ^2)),(1 / ((20 * (T . s)) ^2))*> by A20, TOPREAL6:11 ;
then A21: Sum ((<*(15 * (T . s)),(20 * (T . s))*> ") ^2) = (1 / ((15 * (T . s)) ^2)) + (1 / ((20 * (T . s)) ^2)) by RVSUM_1:77;
(12 (#) T) " = (12 ") (#) (T ") by Th58;
then A22: Sum <*((((12 (#) T) ") ^2) . s)*> = (1 / (12 ^2)) * ((1 / (T . s)) ^2) by A12, A15, VALUED_1:6
.= (1 / (12 ^2)) * ((1 ^2) / ((T . s) ^2)) by XCMPLX_1:76
.= (1 * 1) / ((12 ^2) * ((T . s) ^2)) by XCMPLX_1:76
.= 1 / ((12 * (T . s)) ^2) ;
set p = ((12 (#) T) ") ^2 ;
dom (((12 (#) T) ") ^2) = dom ((12 (#) T) ") by VALUED_1:11;
then A23: len (((12 (#) T) ") ^2) = len ((12 (#) T) ") by FINSEQ_3:29;
dom ((12 (#) T) ") = dom (12 (#) T) by VALUED_1:def 7;
then len ((12 (#) T) ") = len (12 (#) T) by FINSEQ_3:29;
then A24: (((12 (#) T) ") ^2) | ((s - 1) + 1) = ((((12 (#) T) ") ^2) | (s - 1)) ^ <*((((12 (#) T) ") ^2) . ((s - 1) + 1))*> by A6, A7, A23, FINSEQ_5:83, XREAL_1:6;
A25: (((12 ") ^2) (#) ((T ") ^2)) | s = ((12 ") ^2) * (((T ") ^2) | s) by Th56;
A26: (((12 ") (#) (T ")) ^2) | s = (((12 ") ^2) (#) ((T ") ^2)) | s by BORSUK_7:18;
(12 (#) (T | (s - 1))) ^ (<*(15 * (T . s)),(20 * (T . s))*> ^ <*(12 * (T . (s + 1)))*>) = ((12 (#) (T | (s - 1))) ^ <*(15 * (T . s)),(20 * (T . s))*>) ^ <*(12 * (T . (s + 1)))*> by FINSEQ_1:32;
then (X | (s + 1)) " = ((12 (#) (T | (s - 1))) ") ^ (<*(15 * (T . s)),(20 * (T . s))*> ") by A9, Th60;
then ((X | (s + 1)) ") ^2 = (((12 (#) (T | (s - 1))) ") ^2) ^ ((<*(15 * (T . s)),(20 * (T . s))*> ") ^2) by Th59;
hence Sum (((X | (s + 1)) ") ^2) = (Sum (((12 (#) (T | (s - 1))) ") ^2)) + (1 / ((12 * (T . s)) ^2)) by A18, A21, RVSUM_1:75
.= (Sum ((((12 (#) T) ") ^2) | (s - 1))) + (1 / ((12 * (T . s)) ^2)) by A19, Th56
.= Sum (((((12 (#) T) ") ^2) | (s - 1)) ^ <*((((12 (#) T) ") ^2) . s)*>) by A22, RVSUM_1:74
.= Sum ((((12 ") (#) (T ")) ^2) | s) by A24, Th58
.= ((1 ^2) / (12 ^2)) * (1 / ((T . (s + 1)) ^2)) by A3, A13, A14, A25, A26, RVSUM_2:38
.= (1 * 1) / ((12 ^2) * ((T . (s + 1)) ^2)) by XCMPLX_1:76
.= 1 / ((X . ((s + 1) + 1)) ^2) by A11 ;
:: according to NUMBER15:def 12 :: thesis: verum

end;

for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A1, A2);
hence for s being positive Nat ex f being non-empty b₁ + 1 -element natural-valued FinSequence st f is a_solution_of_Sierp168 ; :: thesis: verum