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_2:def 4; :: thesis: verum