deffunc H₁( Element of dom (carr G)) -> Element of the carrier of (G . $1) = the ZeroF of (G . $1);
consider p being non empty FinSequence such that
A9: ( len p = len (carr G) & ( for j being Element of dom (carr G) holds p . j = H₁(j) ) ) from PRVECT_1:sch 1();
A10: ( dom G = Seg (len G) & dom (carr G) = Seg (len (carr G)) & len G = len (carr G) & dom p = Seg (len p) ) by Def4, FINSEQ_1:def 3;

now

let i be set ; :: thesis: ( i in dom (carr G) implies p . i in (carr G) . i )
assume i in dom (carr G) ; :: thesis: p . i in (carr G) . i
then reconsider x = i as Element of dom (carr G) ;
reconsider x' = x as Element of dom G by A10;
( p . x = the ZeroF of (G . x) & (carr G) . x' = the carrier of (G . x') ) by A9, Def4;
hence p . i in (carr G) . i ; :: thesis: verum

end;

then reconsider t = p as Element of product (carr G) by A9, A10, CARD_3:18;
take t ; :: thesis: for j being Element of dom (carr G) holds t . j = the ZeroF of (G . j)
thus for j being Element of dom (carr G) holds t . j = the ZeroF of (G . j) by A9; :: thesis: verum