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

consider p being non empty FinSequence such that

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

take p9 ; :: thesis: ( len p9 = len (carr G) & ( for j being Element of dom (carr G) holds p9 . j = comp (G . j) ) )

thus ( len p9 = len (carr G) & ( for j being Element of dom (carr G) holds p9 . j = comp (G . j) ) ) by A7; :: thesis: verum

consider p being non empty FinSequence such that

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

now :: thesis: for j being Element of dom (carr G) holds p . j is UnOp of ((carr G) . j)

then reconsider p9 = p as UnOps of carr G by A7, PRVECT_1:12;let j be Element of dom (carr G); :: thesis: p . j is UnOp of ((carr G) . j)

len G = len (carr G) by Def4;

then reconsider k = j as Element of dom G by FINSEQ_3:29;

( p . j = comp (G . j) & the carrier of (G . k) = (carr G) . k ) by A7, Def4;

hence p . j is UnOp of ((carr G) . j) ; :: thesis: verum

end;len G = len (carr G) by Def4;

then reconsider k = j as Element of dom G by FINSEQ_3:29;

( p . j = comp (G . j) & the carrier of (G . k) = (carr G) . k ) by A7, Def4;

hence p . j is UnOp of ((carr G) . j) ; :: thesis: verum

take p9 ; :: thesis: ( len p9 = len (carr G) & ( for j being Element of dom (carr G) holds p9 . j = comp (G . j) ) )

thus ( len p9 = len (carr G) & ( for j being Element of dom (carr G) holds p9 . j = comp (G . j) ) ) by A7; :: thesis: verum