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

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

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

end;

hence f = g ; :: thesis: verum