set f = <*1*>;
<*1*> " = <*(1 ")*> by NUMBER15:63;
hence Sum ((<*1*> ") ^2) = Sum <*(1 ^2)*> by RVSUM_1:55
.= 1 ;
:: according to NUMBER17:def 16 :: thesis: verum