deffunc H₁( Element of product (carr G)) -> Element of (G . i) = $1 . i;
consider f being Function of (product (carr G)),(G . i) such that
A1: for x being Element of product (carr G) holds f . x = H₁(x) from FUNCT_2:sch 4();
product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by PRVECT_2:6;
then reconsider f = f as Function of (product G),(G . i) ;
take f ; :: thesis: for x being Element of product (carr G) holds f . x = x . i
thus for x being Element of product (carr G) holds f . x = x . i by A1; :: thesis: verum