let n be Nat; :: thesis: for z being Element of COMPLEX n holds dom z = Seg n
let z be Element of COMPLEX n; :: thesis: dom z = Seg n
len z = n by CARD_1:def 7;
hence dom z = Seg n by FINSEQ_1:def 3; :: thesis: verum