deffunc H₅( Element of dom (carr g)) -> Element of the carrier of (g . $1) = 0. (g . $1);
consider p being non empty FinSequence such that
A9: ( len p = len (carr g) & ( for i being Element of dom (carr g) holds p . i = H₅(i) ) ) 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 Def12, 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 = 0. (g . x) & (carr g) . x' = the carrier of (g . x') ) by A9, Def12;
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 i being Element of dom (carr g) holds t . i = 0. (g . i)
thus for i being Element of dom (carr g) holds t . i = 0. (g . i) by A9; :: thesis: verum