theorem Th143: :: RVSUM_1:143

for f being real-valued FinSequence holds
( len f = len (sqr f) & dom f = dom (sqr f) )