reconsider zz = z as FinSequence by LMPROD1;
dom (carr G) = dom G by ZE;
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