let f, g be Function of the carrier of Y, the carrier of [:X,Y:]; :: thesis: ( ( for r being Element of Y holds f . r = [(x `1),r] ) & ( for r being Element of Y holds g . r = [(x `1),r] ) implies f = g )
assume that
A2: for r being Element of Y holds f . r = [(x `1),r] and
A3: for r being Element of Y holds g . r = [(x `1),r] ; :: thesis: f = g

now :: thesis: for r being Element of Y holds f . r = g . r

let r be Element of Y; :: thesis: f . r = g . r
f . r = [(x `1),r] by A2;
hence f . r = g . r by A3; :: thesis: verum

end;

hence f = g ; :: thesis: verum