let F, G be Function of X,X; :: thesis: ( ( for x being Point of X holds F . x = r * x ) & ( for x being Point of X holds G . x = r * x ) implies F = G )
assume that
A2: for x being Point of X holds F . x = r * x and
A3: for x being Point of X holds G . x = r * x ; :: thesis: F = G
now :: thesis: for x being Point of X holds F . x = G . x
let x be Point of X; :: thesis: F . x = G . x
thus F . x = r * x by A2
.= G . x by A3 ; :: thesis: verum
end;
hence F = G by FUNCT_2:63; :: thesis: verum