deffunc H_{5}( Element of dom (carr g)) -> Element of the carrier of (g . $1) = 0. (g . $1);

A13: dom (carr g) = Seg (len (carr g)) by FINSEQ_1:def 3;

consider p being non empty FinSequence such that

A14: ( len p = len (carr g) & ( for i being Element of dom (carr g) holds p . i = H_{5}(i) ) )
from PRVECT_1:sch 1();

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

then reconsider t = p as Element of product (carr g) by A14, FINSEQ_1:def 3, A16, CARD_3:9;

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

A13: dom (carr g) = Seg (len (carr g)) by FINSEQ_1:def 3;

consider p being non empty FinSequence such that

A14: ( len p = len (carr g) & ( for i being Element of dom (carr g) holds p . i = H

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, A13, Def10;

( p . x = 0. (g . x) & (carr g) . x9 = the carrier of (g . x9) ) by A14, Def10;

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, A13, Def10;

( p . x = 0. (g . x) & (carr g) . x9 = the carrier of (g . x9) ) by A14, Def10;

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

then reconsider t = p as Element of product (carr g) by A14, FINSEQ_1:def 3, A16, CARD_3:9;

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