for f being FinSequence of REAL holds
( len f = len (sqr f) & dom f = dom (sqr f) ) by RVSUM_1:143;