let f be real-valued FinSequence; :: thesis: ( len f = len (sqr f) & dom f = dom (sqr f) )
( rng f c= REAL & dom sqrreal = REAL ) by FUNCT_2:def 1;
hence len f = len (sqrreal * f) by FINSEQ_2:29
.= len (sqr f) ;
:: thesis: dom f = dom (sqr f)
hence dom f = dom (sqr f) by FINSEQ_3:29; :: thesis: verum