let s be positive Nat; :: thesis: for f being s -element natural-valued FinSequence st f is with_sum_of_squares_of_reciprocals_equal_1 holds
(f | (s - 1)) ^ <*(2 * (f . s)),(2 * (f . s)),(2 * (f . s)),(2 * (f . s))*> is with_sum_of_squares_of_reciprocals_equal_1
let f be s -element natural-valued FinSequence; :: thesis: ( f is with_sum_of_squares_of_reciprocals_equal_1 implies (f | (s - 1)) ^ <*(2 * (f . s)),(2 * (f . s)),(2 * (f . s)),(2 * (f . s))*> is with_sum_of_squares_of_reciprocals_equal_1 )
assume A1: f is with_sum_of_squares_of_reciprocals_equal_1 ; :: thesis: (f | (s - 1)) ^ <*(2 * (f . s)),(2 * (f . s)),(2 * (f . s)),(2 * (f . s))*> is with_sum_of_squares_of_reciprocals_equal_1
set g = (f | (s - 1)) ^ <*(2 * (f . s)),(2 * (f . s)),(2 * (f . s)),(2 * (f . s))*>;
<*(2 * (f . s)),(2 * (f . s)),(2 * (f . s)),(2 * (f . s))*> " = <*((2 * (f . s)) "),((2 * (f . s)) "),((2 * (f . s)) "),((2 * (f . s)) ")*> by Th15;
then (<*(2 * (f . s)),(2 * (f . s)),(2 * (f . s)),(2 * (f . s))*> ") ^2 = <*(((2 * (f . s)) ") ^2),(((2 * (f . s)) ") ^2),(((2 * (f . s)) ") ^2),(((2 * (f . s)) ") ^2)*> by Th10;
then A2: Sum ((<*(2 * (f . s)),(2 * (f . s)),(2 * (f . s)),(2 * (f . s))*> ") ^2) = (((((2 * (f . s)) ") ^2) + (((2 * (f . s)) ") ^2)) + (((2 * (f . s)) ") ^2)) + (((2 * (f . s)) ") ^2) by Th20;
A3: ((2 * (f . s)) ") ^2 = ((2 * (f . s)) * (2 * (f . s))) " by XCMPLX_1:204
.= (4 * ((f . s) * (f . s))) "
.= (4 ") * (((f . s) * (f . s)) ") by XCMPLX_1:204 ;
A4: ((f | (s - 1)) ") ^2 = ((f ") | (s - 1)) ^2 by NUMBER15:61
.= ((f ") ^2) | (s - 1) by NUMBER15:62 ;
A5: Sum (((f ") ^2) | (s - 1)) = (Sum ((f ") ^2)) - (((f ") ^2) . s) by Th4;
A6: ((f ") ^2) . s = ((f ") . s) ^2 by VALUED_1:11
.= ((f . s) ") ^2 by VALUED_1:10 ;
((f | (s - 1)) ^ <*(2 * (f . s)),(2 * (f . s)),(2 * (f . s)),(2 * (f . s))*>) " = ((f | (s - 1)) ") ^ (<*(2 * (f . s)),(2 * (f . s)),(2 * (f . s)),(2 * (f . s))*> ") by NUMBER15:60;
then (((f | (s - 1)) ^ <*(2 * (f . s)),(2 * (f . s)),(2 * (f . s)),(2 * (f . s))*>) ") ^2 = (((f | (s - 1)) ") ^2) ^ ((<*(2 * (f . s)),(2 * (f . s)),(2 * (f . s)),(2 * (f . s))*> ") ^2) by NUMBER15:59;
hence Sum ((((f | (s - 1)) ^ <*(2 * (f . s)),(2 * (f . s)),(2 * (f . s)),(2 * (f . s))*>) ") ^2) = (1 - (((f . s) ") ^2)) + ((4 * (4 ")) * (((f . s) * (f . s)) ")) by A1, A2, A3, A4, A5, A6, RVSUM_2:32
.= (1 - (((f . s) ") ^2)) + (4 * (((2 ") * ((f . s) ")) ^2)) by XCMPLX_1:204
.= 1 ;
:: according to NUMBER17:def 16 :: thesis: verum