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
A30: for r being Element of (G . i) holds f . r = x +* (i,r) and
A40: 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 A30;
hence f . r = g . r by A40; :: thesis: verum