deffunc H_{5}( Element of dom (carr g)) -> Element of bool [:[: the carrier of (g . $1), the carrier of (g . $1):], the carrier of (g . $1):] = the addF of (g . $1);

consider p being non empty FinSequence such that

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

take p9 ; :: thesis: ( len p9 = len (carr g) & ( for i being Element of dom (carr g) holds p9 . i = the addF of (g . i) ) )

thus ( len p9 = len (carr g) & ( for i being Element of dom (carr g) holds p9 . i = the addF of (g . i) ) ) by A1; :: thesis: verum

consider p being non empty FinSequence such that

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

now :: thesis: for i being Element of dom (carr g) holds p . i is BinOp of ((carr g) . i)

then reconsider p9 = p as BinOps of carr g by A1, Th11;let i be Element of dom (carr g); :: thesis: p . i is BinOp of ((carr g) . i)

len g = len (carr g) by Def10;

then reconsider j = i as Element of dom g by FINSEQ_3:29;

( p . i = the addF of (g . i) & the carrier of (g . j) = (carr g) . j ) by A1, Def10;

hence p . i is BinOp of ((carr g) . i) ; :: thesis: verum

end;len g = len (carr g) by Def10;

then reconsider j = i as Element of dom g by FINSEQ_3:29;

( p . i = the addF of (g . i) & the carrier of (g . j) = (carr g) . j ) by A1, Def10;

hence p . i is BinOp of ((carr g) . i) ; :: thesis: verum

take p9 ; :: thesis: ( len p9 = len (carr g) & ( for i being Element of dom (carr g) holds p9 . i = the addF of (g . i) ) )

thus ( len p9 = len (carr g) & ( for i being Element of dom (carr g) holds p9 . i = the addF of (g . i) ) ) by A1; :: thesis: verum