deffunc H_{1}( Element of product (carr G)) -> Element of REAL = In (|.(normsequence (G,$1)).|,REAL);

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

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

take f ; :: thesis: for x being Element of product (carr G) holds f . x = |.(normsequence (G,x)).|

let x be Element of product (carr G); :: thesis: f . x = |.(normsequence (G,x)).|

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

hence f . x = |.(normsequence (G,x)).| ; :: thesis: verum

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

A1: for x being Element of product (carr G) holds f . x = H

take f ; :: thesis: for x being Element of product (carr G) holds f . x = |.(normsequence (G,x)).|

let x be Element of product (carr G); :: thesis: f . x = |.(normsequence (G,x)).|

f . x = H

hence f . x = |.(normsequence (G,x)).| ; :: thesis: verum