let x be Point of (product G); :: thesis: x is len G -element
A1: the carrier of (product G) = product (carr G) by Th10;
A2: ( dom x = dom (carr G) & ( for i being set st i in dom (carr G) holds
x . i in (carr G) . i ) ) by A1, CARD_3:9;
len (carr G) = len G by PRVECT_1:def 11;
then dom x = Seg (len G) by A2, FINSEQ_1:def 3;
then len x = len G by FINSEQ_1:def 3;
hence x is len G -element by CARD_1:def 7; :: thesis: verum