deffunc H_{5}( 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_{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 = 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

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

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

then reconsider p9 = p as UnOps of carr g by A7, Th12;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;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

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