set f = <*2,2,2,2*>;
<*2,2,2,2*> " = <*(2 "),(2 "),(2 "),(2 ")*> by Th15;
then (<*2,2,2,2*> ") ^2 = <*((2 ") ^2),((2 ") ^2),((2 ") ^2),((2 ") ^2)*> by Th10;
hence Sum ((<*2,2,2,2*> ") ^2) = (((1 / 4) + (1 / 4)) + (1 / 4)) + (1 / 4) by RVSUM_1:142
.= 1 ;
:: according to NUMBER17:def 16 :: thesis: verum