set f = <*2,2,2,3,3,7,14,21*>;
<*2,2,2,3,3,7,14,21*> " = <*(2 "),(2 "),(2 "),(3 "),(3 "),(7 "),(14 "),(21 ")*> by Th19;
then (<*2,2,2,3,3,7,14,21*> ") ^2 = <*((2 ") ^2),((2 ") ^2),((2 ") ^2),((3 ") ^2),((3 ") ^2),((7 ") ^2),((14 ") ^2),((21 ") ^2)*> by Th14;
hence Sum ((<*2,2,2,3,3,7,14,21*> ") ^2) = (((((((1 / 4) + (1 / 4)) + (1 / 4)) + (1 / 9)) + (1 / 9)) + (1 / 49)) + (1 / 196)) + (1 / 441) by Th24
.= 1 ;
:: according to NUMBER17:def 16 :: thesis: verum