let a be Real; :: thesis: for i being Nat
for F being FinSequence of REAL st i in dom (abs F) & a = F . i holds
(abs F) . i = |.a.|
let i be Nat; :: thesis: for F being FinSequence of REAL st i in dom (abs F) & a = F . i holds
(abs F) . i = |.a.|
let F be FinSequence of REAL ; :: thesis: ( i in dom (abs F) & a = F . i implies (abs F) . i = |.a.| )
assume that
A1: i in dom (abs F) and
A2: a = F . i ; :: thesis: (abs F) . i = |.a.|
(abs F) . i = absreal . a by A1, A2, FUNCT_1:12;
hence (abs F) . i = |.a.| by EUCLID:def 2; :: thesis: verum