deffunc H_{1}( Element of dom G) -> Element of REAL = In (( the normF of (G . $1) . (x . $1)),REAL);

consider f being Function of (dom G),REAL such that

A1: for j being Element of dom G holds f . j = H_{1}(j)
from FUNCT_2:sch 4();

A2: rng f c= REAL ;

dom f = dom G by FUNCT_2:def 1;

then A3: dom f = Seg (len G) by FINSEQ_1:def 3;

then f is FinSequence by FINSEQ_1:def 2;

then reconsider f = f as FinSequence of REAL by A2, FINSEQ_1:def 4;

A4: f in REAL * by FINSEQ_1:def 11;

len f = len G by A3, FINSEQ_1:def 3;

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 normF of (G . j) . (x . j) ) )

thus len f = len G by CARD_1:def 7; :: thesis: for j being Element of dom G holds f . j = the normF of (G . j) . (x . j)

let j be Element of dom G; :: thesis: f . j = the normF of (G . j) . (x . j)

f . j = H_{1}(j)
by A1;

hence f . j = the normF of (G . j) . (x . j) ; :: thesis: verum

consider f being Function of (dom G),REAL such that

A1: for j being Element of dom G holds f . j = H

A2: rng f c= REAL ;

dom f = dom G by FUNCT_2:def 1;

then A3: dom f = Seg (len G) by FINSEQ_1:def 3;

then f is FinSequence by FINSEQ_1:def 2;

then reconsider f = f as FinSequence of REAL by A2, FINSEQ_1:def 4;

A4: f in REAL * by FINSEQ_1:def 11;

len f = len G by A3, FINSEQ_1:def 3;

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 normF of (G . j) . (x . j) ) )

thus len f = len G by CARD_1:def 7; :: thesis: for j being Element of dom G holds f . j = the normF of (G . j) . (x . j)

let j be Element of dom G; :: thesis: f . j = the normF of (G . j) . (x . j)

f . j = H

hence f . j = the normF of (G . j) . (x . j) ; :: thesis: verum