let s, n be Nat; for f being s + 1 -element complex-valued FinSequence st f is a_solution_of_Sierp168 holds
n (#) f is a_solution_of_Sierp168
let f be s + 1 -element complex-valued FinSequence; ( f is a_solution_of_Sierp168 implies n (#) f is a_solution_of_Sierp168 )
assume A1:
Sum (((f | s) ") ^2) = 1 / ((f . (s + 1)) ^2)
; NUMBER15:def 12 n (#) f is a_solution_of_Sierp168
set g = n (#) f;
A2:
(n (#) f) . (s + 1) = n * (f . (s + 1))
by VALUED_1:6;
A3:
(n (#) (f | s)) ^2 = (n ^2) (#) ((f | s) ^2)
by BORSUK_7:18;
A4:
((f | s) ") ^2 = ((f | s) ^2) "
by Th57;
A5:
((n (#) (f | s)) ") ^2 = ((n (#) (f | s)) ^2) "
by Th57;
A6:
((n ^2) (#) ((f | s) ^2)) " = (1 / (n ^2)) (#) (((f | s) ^2) ")
by Th58;
(n (#) f) | s = n (#) (f | s)
by Th56;
hence Sum ((((n (#) f) | s) ") ^2) =
(1 / (n ^2)) * (Sum (((f | s) ^2) "))
by A3, A5, A6, RVSUM_2:38
.=
(1 * 1) / ((n ^2) * ((f . (s + 1)) ^2))
by A1, A4, XCMPLX_1:76
.=
1 / (((n (#) f) . (s + 1)) ^2)
by A2
;
NUMBER15:def 12 verum