deffunc H₁( Element of dom G) -> Element of REAL = the norm of (G . $1) . (x . $1);
consider f being Function of (dom G),REAL such that
A1: for j being Element of dom G holds f . j = H₁(j) from FUNCT_2:sch 4();
dom f = dom G by FUNCT_2:def 1;
then A2: dom f = Seg (len G) by FINSEQ_1:def 3;
then A3: f is FinSequence by FINSEQ_1:def 2;
rng f c= REAL ;
then reconsider f = f as FinSequence of REAL by A3, FINSEQ_1:def 4;
A4: len f = len G by A2, FINSEQ_1:def 3;
f in REAL * by FINSEQ_1:def 11;
then f in (len G) -tuples_on REAL by A4;
then reconsider f = f as Element of REAL (len G) ;
take f ; :: thesis: ( len f = len G & ( for j being Element of dom G holds f . j = the norm of (G . j) . (x . j) ) )
thus len f = len G by FINSEQ_1:def 18; :: thesis: for j being Element of dom G holds f . j = the norm of (G . j) . (x . j)
let j be Element of dom G; :: thesis: f . j = the norm of (G . j) . (x . j)
thus f . j = the norm of (G . j) . (x . j) by A1; :: thesis: verum