let F, G be Function of X,X; :: thesis: ( ( for x being Point of X holds F . x = a + x ) & ( for x being Point of X holds G . x = a + x ) implies F = G )
assume that
A2: for x being Point of X holds F . x = a + x and
A3: for x being Point of X holds G . x = a + x ; :: thesis: F = G

now

let x be Point of X; :: thesis: F . x = G . x
thus F . x = a + x by A2
.= G . x by A3 ; :: thesis: verum

end;

hence F = G by FUNCT_2:113; :: thesis: verum