deffunc H5( 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 = H5(i) ) ) from PRVECT_1:sch 1();
now :: thesis: for i being Element of dom (carr g) holds p . i is BinOp of ((carr g) . i)
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;
then reconsider p9 = p as BinOps of carr g by A1, Th11;
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