let f be FinSequence of REAL ; :: thesis: ( len f = len (abs f) & dom f = dom (abs f) )
( rng f c= REAL & dom absreal = REAL ) by FUNCT_2:def 1;
hence len f = len (abs f) by FINSEQ_2:33; :: thesis: dom f = dom (abs f)
hence dom f = dom (abs f) by FINSEQ_3:31; :: thesis: verum