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