let n be Nat; for s being positive Nat
for f being b1 + 1 -element complex-valued FinSequence st f is a_solution_of_Sierp169 holds
n (#) f is a_solution_of_Sierp169
let s be positive Nat; for f being s + 1 -element complex-valued FinSequence st f is a_solution_of_Sierp169 holds
n (#) f is a_solution_of_Sierp169
let f be s + 1 -element complex-valued FinSequence; ( f is a_solution_of_Sierp169 implies n (#) f is a_solution_of_Sierp169 )
assume A1:
f is a_solution_of_Sierp169
; n (#) f is a_solution_of_Sierp169
set g = n (#) f;
A2:
( (f . (s + 1)) |^ 3 = ((f . (s + 1)) * (f . (s + 1))) * (f . (s + 1)) & ((n (#) f) . (s + 1)) |^ 3 = (((n (#) f) . (s + 1)) * ((n (#) f) . (s + 1))) * ((n (#) f) . (s + 1)) )
by POLYEQ_5:2;
A3:
(n (#) f) . (s + 1) = n * (f . (s + 1))
by VALUED_1:6;
A4:
(n (#) f) | s = n (#) (f | s)
by NUMBER15:56;
then
((n (#) f) | s) (#) ((n (#) f) | s) = (n * n) (#) ((f | s) (#) (f | s))
by Th51;
then A5:
(((n (#) f) | s) (#) ((n (#) f) | s)) (#) ((n (#) f) | s) = ((n * n) * n) (#) (((f | s) (#) (f | s)) (#) (f | s))
by A4, Th51;
(((n * n) * n) (#) (((f | s) (#) (f | s)) (#) (f | s))) " = (((n * n) * n) ") (#) ((((f | s) (#) (f | s)) (#) (f | s)) ")
by NUMBER15:58;
hence Sum (((((n (#) f) | s) (#) ((n (#) f) | s)) (#) ((n (#) f) | s)) ") =
(1 / ((n * n) * n)) * (1 / ((f . (s + 1)) |^ 3))
by A1, A5, RVSUM_2:38
.=
1 / (((n * n) * n) * ((f . (s + 1)) |^ 3))
by XCMPLX_1:102
.=
1 / (((n (#) f) . (s + 1)) |^ 3)
by A2, A3
;
NUMBER17:def 17 verum