deffunc H_{1}( 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

A13: ( len p = len (carr G) & ( for j being Element of dom (carr G) holds p . j = H_{1}(j) ) )
from PRVECT_1:sch 1();

A14: dom (carr G) = Seg (len (carr G)) by FINSEQ_1:def 3;

A15: dom G = Seg (len G) by FINSEQ_1:def 3;

then reconsider t = p as Element of product (carr G) by A13, A14, A16, CARD_3:9;

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 A13; :: thesis: verum

consider p being non empty FinSequence such that

A13: ( len p = len (carr G) & ( for j being Element of dom (carr G) holds p . j = H

A14: dom (carr G) = Seg (len (carr G)) by FINSEQ_1:def 3;

A15: dom G = Seg (len G) by FINSEQ_1:def 3;

A16: now :: thesis: for i being object st i in dom (carr G) holds

p . i in (carr G) . i

dom p = Seg (len p)
by FINSEQ_1:def 3;p . i in (carr G) . i

let i be object ; :: 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 x9 = x as Element of dom G by A15, A14, Def4;

( p . x = the ZeroF of (G . x) & (carr G) . x9 = the carrier of (G . x9) ) by A13, Def4;

hence p . i in (carr G) . i ; :: thesis: verum

end;assume i in dom (carr G) ; :: thesis: p . i in (carr G) . i

then reconsider x = i as Element of dom (carr G) ;

reconsider x9 = x as Element of dom G by A15, A14, Def4;

( p . x = the ZeroF of (G . x) & (carr G) . x9 = the carrier of (G . x9) ) by A13, Def4;

hence p . i in (carr G) . i ; :: thesis: verum

then reconsider t = p as Element of product (carr G) by A13, A14, A16, CARD_3:9;

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 A13; :: thesis: verum