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:29; :: thesis: dom f = dom (abs f)
hence dom f = dom (abs f) by FINSEQ_3:29; :: thesis: verum