let n, k be Nat; :: thesis: for r being real number
for x being Element of REAL n st r = x . k holds
(abs x) . k = abs r
let r be real number ; :: thesis: for x being Element of REAL n st r = x . k holds
(abs x) . k = abs r
let x be Element of REAL n; :: thesis: ( r = x . k implies (abs x) . k = abs r )
assume A1: r = x . k ; :: thesis: (abs x) . k = abs r

per cases ( k in Seg n or not k in Seg n ) ;

suppose A2: k in Seg n ; :: thesis: (abs x) . k = abs r

len (abs x) = n by FINSEQ_1:def 18;
then ( absreal * x = abs x & k in dom (abs x) ) by A2, FINSEQ_1:def 3;
hence (abs x) . k = absreal . r by A1, FUNCT_1:22
.= abs r by Def2 ;
:: thesis: verum

end;

suppose A3: not k in Seg n ; :: thesis: (abs x) . k = abs r

then A4: not k in dom x by Th3;
A5: not k in dom (abs x) by A3, Th3;
A6: r = {} by A1, A4, FUNCT_1:def 4;
(abs x) . k = 0 by A5, FUNCT_1:def 4;
hence (abs x) . k = abs r by A6, ABSVALUE:def 1; :: thesis: verum

end;

end;