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

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

let i be Element of dom (carr g); :: thesis: p . i is UnOp 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 = comp (g . i) & the carrier of (g . j) = (carr g) . j ) by A7, Def10;
hence p . i is UnOp of ((carr g) . i) ; :: thesis: verum

end;

then reconsider p9 = p as UnOps of carr g by A7, Th12;
take p9 ; :: thesis: ( len p9 = len (carr g) & ( for i being Element of dom (carr g) holds p9 . i = comp (g . i) ) )
thus ( len p9 = len (carr g) & ( for i being Element of dom (carr g) holds p9 . i = comp (g . i) ) ) by A7; :: thesis: verum