let k, n be Nat; :: thesis: for c being Element of COMPLEX
for z being Element of COMPLEX n st k in Seg n & c = z . k holds
(abs z) . k = |.c.|
let c be Element of COMPLEX ; :: thesis: for z being Element of COMPLEX n st k in Seg n & c = z . k holds
(abs z) . k = |.c.|
let z be Element of COMPLEX n; :: thesis: ( k in Seg n & c = z . k implies (abs z) . k = |.c.| )
assume that
A1: k in Seg n and
A2: c = z . k ; :: thesis: (abs z) . k = |.c.|
len (abs z) = n by CARD_1:def 7;
then k in dom (abs z) by A1, FINSEQ_1:def 3;
hence (abs z) . k = abscomplex . c by A2, FUNCT_1:12
.= |.c.| by Def5 ;
:: thesis: verum