set g = absreal * x;
dom absreal = REAL by FUNCT_2:def 1;
then rng x c= dom absreal ;
then A1: ( dom (abs x) = dom x & dom (absreal * x) = dom x ) by RELAT_1:27, VALUED_1:def 11;

now :: thesis: for a being object st a in dom (abs x) holds
(abs x) . a = (absreal * x) . a

let a be object ; :: thesis: ( a in dom (abs x) implies (abs x) . a = (absreal * x) . a )
assume A2: a in dom (abs x) ; :: thesis: (abs x) . a = (absreal * x) . a
thus (abs x) . a = |.(x . a).| by VALUED_1:18
.= absreal . (x . a) by Def2
.= (absreal * x) . a by A1, A2, FUNCT_1:12 ; :: thesis: verum

end;

hence for b₁ being FinSequence of REAL holds
( b₁ = |.x.| iff b₁ = absreal * x ) by A1, FUNCT_1:2; :: thesis: verum