theorem Th143: :: RVSUM_1:143

for f being FinSequence of REAL holds
( len f = len (sqr f) & dom f = dom (sqr f) )