deffunc H₁( 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 j being Element of dom (carr G) holds p . j = H₁(j) ) ) from PRVECT_1:sch 1();

now

let j be Element of dom (carr G); :: thesis: p . j is BinOp of ((carr G) . j)
len G = len (carr G) by Def4;
then reconsider k = j as Element of dom G by FINSEQ_3:31;
( p . j = the addF of (G . j) & the carrier of (G . k) = (carr G) . k ) by A1, Def4;
hence p . j is BinOp of ((carr G) . j) ; :: thesis: verum

end;

then reconsider p9 = p as BinOps of carr G by A1, PRVECT_1:19;
take p9 ; :: thesis: ( len p9 = len (carr G) & ( for j being Element of dom (carr G) holds p9 . j = the addF of (G . j) ) )
thus ( len p9 = len (carr G) & ( for j being Element of dom (carr G) holds p9 . j = the addF of (G . j) ) ) by A1; :: thesis: verum