let f, g be Function of (X . i),(product X); :: thesis: ( ( for r being object st r in X . i holds
f . r = x +* (i,r) ) & ( for r being object st r in X . i holds
g . r = x +* (i,r) ) implies f = g )
assume that
A10: for r being object st r in X . i holds
f . r = x +* (i,r) and
A11: for r being object st r in X . i holds
g . r = x +* (i,r) ; :: thesis: f = g

now :: thesis: for r being object st r in X . i holds
f . r = g . r

let r be object ; :: thesis: ( r in X . i implies f . r = g . r )
assume A12: r in X . i ; :: thesis: f . r = g . r
hence f . r = x +* (i,r) by A10
.= g . r by A11, A12 ;
:: thesis: verum

end;

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