( dom G = Seg (len G) & Seg (len (carr G)) = dom (carr G) ) by FINSEQ_1:def 3;
then reconsider j9 = j as Element of dom G by PRVECT_1:def 11;
G . j9 is VectSp of K ;
hence G . j is VectSp of K ; :: thesis: verum