reconsider zz = z as FinSequence by Th9;
dom (carr G) = dom G by Lm1;
then zz . j in (carr G) . j by CARD_3:9;
hence z . j is Element of (G . j) by PRVECT_1:def 11; :: thesis: verum