let n be Nat; :: thesis: for x being Element of REAL n
for i being Nat st i in Seg n holds
(abs x) . i in REAL
let x be Element of REAL n; :: thesis: for i being Nat st i in Seg n holds
(abs x) . i in REAL
let i be Nat; :: thesis: ( i in Seg n implies (abs x) . i in REAL )
assume A1: i in Seg n ; :: thesis: (abs x) . i in REAL
reconsider f = x as complex-valued Function ;
( dom |.f.| = dom f & dom f = Seg n ) by FINSEQ_2:124, VALUED_1:def 11;
then ( rng |.f.| c= REAL & i in dom |.f.| ) by A1;
hence (abs x) . i in REAL by FUNCT_1:3; :: thesis: verum