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
A2: for x being Element of product (carr G) holds f . x = x . i and
A3: for x being Element of product (carr G) holds g . x = x . i ; :: thesis: f = g
A4: product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by PRVECT_2:6;
now :: thesis: for x1 being Element of the carrier of (product G) holds f . x1 = g . x1
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 A4;
f . x1 = x . i by A2;
hence f . x1 = g . x1 by A3; :: thesis: verum
end;
hence f = g ; :: thesis: verum