let s be positive Nat; :: thesis: for f being s + 1 -element complex-valued FinSequence st f is a_solution_of_Sierp169 holds
(10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*> is a_solution_of_Sierp169
let f be s + 1 -element complex-valued FinSequence; :: thesis: ( f is a_solution_of_Sierp169 implies (10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*> is a_solution_of_Sierp169 )
assume A1: f is a_solution_of_Sierp169 ; :: thesis: (10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*> is a_solution_of_Sierp169
set x = f . s;
set y = f . (s + 1);
set a = 12 * (f . s);
set b = 15 * (f . s);
set c = 20 * (f . s);
set d = 10 * (f . (s + 1));
set F = <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*>;
set G = <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>;
set J = <*(10 * (f . (s + 1)))*>;
set S1 = f | (s - 1);
set Z = 10 (#) (f | (s - 1));
set g = (10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>;
set f1 = (10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*>;
set h = ((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>) | (s + 2);
A2: (10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*> = ((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*>) ^ <*(10 * (f . (s + 1)))*> by FINSEQ_1:32;
A3: len f = s + 1 by CARD_1:def 7;
A4: len (f | (s - 1)) = len (10 (#) (f | (s - 1))) by COMPLSP2:3;
s - 1 <= s by XREAL_1:147;
then s - 1 <= s + 1 by XREAL_1:145;
then A5: len (10 (#) (f | (s - 1))) = s - 1 by A3, A4, FINSEQ_1:59;
len <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*> = 3 by CARD_1:def 7;
then A6: s + 2 = (len (10 (#) (f | (s - 1)))) + (len <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*>) by A5
.= len ((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*>) by FINSEQ_1:22 ;
then A7: (((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>) | (s + 2)) " = ((10 (#) (f | (s - 1))) ") ^ (<*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*> ") by A2, NUMBER15:60;
((((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>) | (s + 2)) (#) (((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>) | (s + 2))) " = ((((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>) | (s + 2)) ") (#) ((((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>) | (s + 2)) ") by Th50;
then A8: (((((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>) | (s + 2)) (#) (((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>) | (s + 2))) (#) (((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>) | (s + 2))) " = (((((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>) | (s + 2)) ") (#) ((((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>) | (s + 2)) ")) (#) ((((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>) | (s + 2)) ") by Th50;
A9: (((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>) . (s + 3)) |^ 3 = ((((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>) . (s + 3)) * (((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>) . (s + 3))) * (((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>) . (s + 3)) by POLYEQ_5:2;
len ((10 (#) (f | (s - 1))) ") = len ((10 (#) (f | (s - 1))) ") ;
then A10: ((((10 (#) (f | (s - 1))) ") ^ (<*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*> ")) (#) (((10 (#) (f | (s - 1))) ") ^ (<*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*> "))) (#) (((10 (#) (f | (s - 1))) ") ^ (<*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*> ")) = ((((10 (#) (f | (s - 1))) ") (#) ((10 (#) (f | (s - 1))) ")) ^ ((<*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*> ") (#) (<*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*> "))) (#) (((10 (#) (f | (s - 1))) ") ^ (<*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*> ")) by EULRPART:8;
consider k being Nat such that
A11: s = k + 1 by NAT_1:6;
A12: (f | s) | k = f | k by A11, FINSEQ_1:82, NAT_1:11;
A13: (f | s) . s = f . s by FINSEQ_3:112;
<*(f . s)*> (#) <*(f . s)*> = <*((f . s) * (f . s))*> by RVSUM_2:26;
then A14: (<*(f . s)*> (#) <*(f . s)*>) (#) <*(f . s)*> = <*(((f . s) * (f . s)) * (f . s))*> by RVSUM_2:26;
len (f | (s - 1)) = len (f | (s - 1)) ;
then A15: (((f | (s - 1)) ^ <*(f . s)*>) (#) ((f | (s - 1)) ^ <*(f . s)*>)) (#) ((f | (s - 1)) ^ <*(f . s)*>) = (((f | (s - 1)) (#) (f | (s - 1))) (#) (f | (s - 1))) ^ ((<*(f . s)*> (#) <*(f . s)*>) (#) <*(f . s)*>) by Th52;
A16: <*(((f . s) * (f . s)) * (f . s))*> " = <*((((f . s) * (f . s)) * (f . s)) ")*> by NUMBER15:63;
len (f | s) = s by CARD_1:def 7;
then f | s = (f | (s - 1)) ^ <*(f . s)*> by A11, A12, A13, RFINSEQ:7;
then (((f | s) (#) (f | s)) (#) (f | s)) " = ((((f | (s - 1)) (#) (f | (s - 1))) (#) (f | (s - 1))) ") ^ (<*(((f . s) * (f . s)) * (f . s))*> ") by A14, A15, NUMBER15:60;
then A17: (Sum ((((f | (s - 1)) (#) (f | (s - 1))) (#) (f | (s - 1))) ")) + (Sum <*((((f . s) * (f . s)) * (f . s)) ")*>) = 1 / ((f . (s + 1)) |^ 3) by A1, A16, RVSUM_2:32;
A18: (10 (#) (f | (s - 1))) " = (10 ") (#) ((f | (s - 1)) ") by NUMBER15:58;
((f | (s - 1)) (#) (f | (s - 1))) " = ((f | (s - 1)) ") (#) ((f | (s - 1)) ") by Th50;
then A19: (((f | (s - 1)) (#) (f | (s - 1))) (#) (f | (s - 1))) " = (((f | (s - 1)) ") (#) ((f | (s - 1)) ")) (#) ((f | (s - 1)) ") by Th50;
((10 ") (#) ((f | (s - 1)) ")) (#) ((10 ") (#) ((f | (s - 1)) ")) = ((10 ") * (10 ")) (#) (((f | (s - 1)) ") (#) ((f | (s - 1)) ")) by Th51;
then A20: (((10 ") (#) ((f | (s - 1)) ")) (#) ((10 ") (#) ((f | (s - 1)) "))) (#) ((10 ") (#) ((f | (s - 1)) ")) = (((10 ") * (10 ")) * (10 ")) (#) ((((f | (s - 1)) ") (#) ((f | (s - 1)) ")) (#) ((f | (s - 1)) ")) by Th51;
A21: (f . (s + 1)) |^ 3 = ((f . (s + 1)) * (f . (s + 1))) * (f . (s + 1)) by POLYEQ_5:2;
A22: <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*> " = <*((12 * (f . s)) "),((15 * (f . s)) "),((20 * (f . s)) ")*> by NUMBER15:65;
then (<*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*> ") (#) (<*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*> ") = <*(((12 * (f . s)) ") * ((12 * (f . s)) ")),(((15 * (f . s)) ") * ((15 * (f . s)) ")),(((20 * (f . s)) ") * ((20 * (f . s)) "))*> by FINSEQ_9:46;
then ((<*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*> ") (#) (<*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*> ")) (#) (<*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*> ") = <*((((12 * (f . s)) ") * ((12 * (f . s)) ")) * ((12 * (f . s)) ")),((((15 * (f . s)) ") * ((15 * (f . s)) ")) * ((15 * (f . s)) ")),((((20 * (f . s)) ") * ((20 * (f . s)) ")) * ((20 * (f . s)) "))*> by A22, FINSEQ_9:46;
then A23: Sum (((<*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*> ") (#) (<*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*> ")) (#) (<*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*> ")) = (((((12 * (f . s)) ") * ((12 * (f . s)) ")) * ((12 * (f . s)) ")) + ((((15 * (f . s)) ") * ((15 * (f . s)) ")) * ((15 * (f . s)) "))) + ((((20 * (f . s)) ") * ((20 * (f . s)) ")) * ((20 * (f . s)) ")) by RVSUM_2:35;

now :: thesis: for c1, c2, c3 being Complex holds ((c1 * c2) * c3) " = ((c1 ") * (c2 ")) * (c3 ")

let c1, c2, c3 be Complex; :: thesis: ((c1 * c2) * c3) " = ((c1 ") * (c2 ")) * (c3 ")
thus ((c1 * c2) * c3) " = ((c1 * c2) ") * (c3 ") by XCMPLX_1:204
.= ((c1 ") * (c2 ")) * (c3 ") by XCMPLX_1:204 ; :: thesis: verum

end;

then A24: ( (((12 * (f . s)) ") * ((12 * (f . s)) ")) * ((12 * (f . s)) ") = (((12 * (f . s)) * (12 * (f . s))) * (12 * (f . s))) " & (((15 * (f . s)) ") * ((15 * (f . s)) ")) * ((15 * (f . s)) ") = (((15 * (f . s)) * (15 * (f . s))) * (15 * (f . s))) " & (((20 * (f . s)) ") * ((20 * (f . s)) ")) * ((20 * (f . s)) ") = (((20 * (f . s)) * (20 * (f . s))) * (20 * (f . s))) " ) ;
A25: ((((f . s) * (f . s)) * (f . s)) ") * (((12 * 12) * 12) ") = ((((f . s) * (f . s)) * (f . s)) * ((12 * 12) * 12)) " by XCMPLX_1:204
.= (((12 * (f . s)) * (12 * (f . s))) * (12 * (f . s))) " ;
A26: ((((f . s) * (f . s)) * (f . s)) ") * (((15 * 15) * 15) ") = ((((f . s) * (f . s)) * (f . s)) * ((15 * 15) * 15)) " by XCMPLX_1:204
.= (((15 * (f . s)) * (15 * (f . s))) * (15 * (f . s))) " ;
A27: ((((f . s) * (f . s)) * (f . s)) ") * (((20 * 20) * 20) ") = ((((f . s) * (f . s)) * (f . s)) * ((20 * 20) * 20)) " by XCMPLX_1:204
.= (((20 * (f . s)) * (20 * (f . s))) * (20 * (f . s))) " ;
dom (((10 (#) (f | (s - 1))) ") (#) ((10 (#) (f | (s - 1))) ")) = (dom ((10 (#) (f | (s - 1))) ")) /\ (dom ((10 (#) (f | (s - 1))) ")) by VALUED_1:def 4
.= dom ((10 (#) (f | (s - 1))) ") ;
then len (((10 (#) (f | (s - 1))) ") (#) ((10 (#) (f | (s - 1))) ")) = len ((10 (#) (f | (s - 1))) ") by FINSEQ_3:29;
then (((((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>) | (s + 2)) (#) (((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>) | (s + 2))) (#) (((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>) | (s + 2))) " = ((((10 (#) (f | (s - 1))) ") (#) ((10 (#) (f | (s - 1))) ")) (#) ((10 (#) (f | (s - 1))) ")) ^ (((<*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*> ") (#) (<*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*> ")) (#) (<*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*> ")) by A7, A8, A10, EULRPART:8;
hence Sum ((((((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>) | (s + 2)) (#) (((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>) | (s + 2))) (#) (((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>) | (s + 2))) ") = (Sum ((((10 (#) (f | (s - 1))) ") (#) ((10 (#) (f | (s - 1))) ")) (#) ((10 (#) (f | (s - 1))) "))) + (Sum (((<*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*> ") (#) (<*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*> ")) (#) (<*(12 * (f . s)),(15 * (f . s)),(20 * (f . s))*> "))) by RVSUM_2:32
.= (((Sum ((((10 (#) (f | (s - 1))) ") (#) ((10 (#) (f | (s - 1))) ")) (#) ((10 (#) (f | (s - 1))) "))) + ((((12 * (f . s)) ") * ((12 * (f . s)) ")) * ((12 * (f . s)) "))) + ((((15 * (f . s)) ") * ((15 * (f . s)) ")) * ((15 * (f . s)) "))) + ((((20 * (f . s)) ") * ((20 * (f . s)) ")) * ((20 * (f . s)) ")) by A23
.= ((((1000 ") * ((1 / (((f . (s + 1)) * (f . (s + 1))) * (f . (s + 1)))) - ((((f . s) * (f . s)) * (f . s)) "))) + ((((12 * (f . s)) ") * ((12 * (f . s)) ")) * ((12 * (f . s)) "))) + ((((15 * (f . s)) ") * ((15 * (f . s)) ")) * ((15 * (f . s)) "))) + ((((20 * (f . s)) ") * ((20 * (f . s)) ")) * ((20 * (f . s)) ")) by A17, A18, A19, A20, A21, RVSUM_2:38
.= (1 / 1000) * (1 / (((f . (s + 1)) * (f . (s + 1))) * (f . (s + 1)))) by A24, A25, A26, A27
.= 1 / (1000 * (((f . (s + 1)) * (f . (s + 1))) * (f . (s + 1)))) by XCMPLX_1:102
.= 1 / ((((10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>) . ((s + 2) + 1)) |^ 3) by A2, A6, A9 ;
:: according to NUMBER17:def 17 :: thesis: verum