let f be complex-valued FinSequence; :: thesis: ( f is with_sum_of_reciprocals_equal_1 implies Sierp162FS f is with_sum_of_reciprocals_equal_1 )
assume A1: f is with_sum_of_reciprocals_equal_1 ; :: thesis: Sierp162FS f is with_sum_of_reciprocals_equal_1
set g = Sierp162FS f;
set F = 2 (#) f;
A2: (2 (#) f) " = (2 ") (#) (f ") by NUMBER15:58;
A3: <*2*> " = <*(2 ")*> by NUMBER15:63;
A4: Sum ((2 ") (#) (f ")) = (2 ") * (Sum (f ")) by RVSUM_2:38;
(Sierp162FS f) " = (<*2*> ") ^ ((2 (#) f) ") by NUMBER15:60;
hence Sum ((Sierp162FS f) ") = (Sum (<*2*> ")) + (Sum ((2 (#) f) ")) by RVSUM_2:32
.= 1 by A1, A2, A3, A4 ;
:: according to NUMBER17:def 6 :: thesis: verum