deffunc H₁( Element of dom (carr G)) -> Element of bool [:[:REAL ,the carrier of (G . $1):],the carrier of (G . $1):] = the Mult of (G . $1);
consider p being non empty FinSequence such that
A14: ( 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 ai be set ; :: thesis: ( ai in dom (carr G) implies p . ai is Function of [:REAL ,((carr G) . ai):],((carr G) . ai) )
assume ai in dom (carr G) ; :: thesis: p . ai is Function of [:REAL ,((carr G) . ai):],((carr G) . ai)
then reconsider i = ai as Element of dom (carr G) ;
len G = len (carr G) by Def4;
then reconsider j = i as Element of dom G by FINSEQ_3:31;
( p . i = the Mult of (G . i) & the carrier of (G . j) = (carr G) . j ) by A14, Def4;
hence p . ai is Function of [:REAL ,((carr G) . ai):],((carr G) . ai) ; :: thesis: verum

end;

then reconsider p' = p as MultOps of REAL , carr G by A14, Th4;
take p' ; :: thesis: ( len p' = len (carr G) & ( for j being Element of dom (carr G) holds p' . j = the Mult of (G . j) ) )
thus ( len p' = len (carr G) & ( for j being Element of dom (carr G) holds p' . j = the Mult of (G . j) ) ) by A14; :: thesis: verum