deffunc H₁( 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₁(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₁(j) by A1;
hence f . j = the normF of (G . j) . (x . j) ; :: thesis: verum