let k, n be Nat; :: thesis: for z being Element of COMPLEX n st k in Seg n holds
z . k in COMPLEX
let z be Element of COMPLEX n; :: thesis: ( k in Seg n implies z . k in COMPLEX )
len z = n by CARD_1:def 7;
then Seg n = dom z by FINSEQ_1:def 3;
hence ( k in Seg n implies z . k in COMPLEX ) by FINSEQ_2:11; :: thesis: verum