deffunc H_{1}( 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

A20: ( 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 = the Mult of (G . j) ) )

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

consider p being non empty FinSequence such that

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

now :: thesis: for ai being set st ai in dom (carr G) holds

p . ai is Function of [:REAL,((carr G) . ai):],((carr G) . ai)

then reconsider p9 = p as MultOps of REAL , carr G by A20, Th4;p . ai is Function of [:REAL,((carr G) . ai):],((carr G) . ai)

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:29;

( p . i = the Mult of (G . i) & the carrier of (G . j) = (carr G) . j ) by A20, Def4;

hence p . ai is Function of [:REAL,((carr G) . ai):],((carr G) . ai) ; :: thesis: verum

end;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:29;

( p . i = the Mult of (G . i) & the carrier of (G . j) = (carr G) . j ) by A20, Def4;

hence p . ai is Function of [:REAL,((carr G) . ai):],((carr G) . ai) ; :: thesis: verum

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

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