( 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 RealLinearSpace ;
hence G . j is RealLinearSpace ; :: thesis: verum