let f, g be Function of the carrier of (product G), the carrier of (G . i); :: thesis: ( ( for x being Element of product (carr G) holds f . x = x . i ) & ( for x being Element of product (carr G) holds g . x = x . i ) implies f = g )
assume that
A1: for x being Element of product (carr G) holds f . x = x . i and
A2: for x being Element of product (carr G) holds g . x = x . i ; :: thesis: f = g
A3: product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by PRVECT_2:6;

now

let x1 be Element of the carrier of (product G); :: thesis: f . x1 = g . x1
reconsider x = x1 as Element of product (carr G) by A3;
f . x1 = x . i by A1;
hence f . x1 = g . x1 by A2; :: thesis: verum

end;

hence f = g by FUNCT_2:63; :: thesis: verum