let f, g be Function of the carrier of (G . i), the carrier of (product G); :: thesis: ( ( for r being Element of (G . i) holds f . r = x +* (i,r) ) & ( for r being Element of (G . i) holds g . r = x +* (i,r) ) implies f = g )
assume that
A2: for r being Element of (G . i) holds f . r = x +* (i,r) and
A3: for r being Element of (G . i) holds g . r = x +* (i,r) ; :: thesis: f = g
let r be Element of (G . i); :: according to FUNCT_2:def 8 :: thesis: f . r = g . r
f . r = x +* (i,r) by A2;
hence f . r = g . r by A3; :: thesis: verum