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