let X be non empty set ; :: thesis: for f being Function of X,X st ( for x being Element of X holds f . x = x ) holds
f = id X
let f be Function of X,X; :: thesis: ( ( for x being Element of X holds f . x = x ) implies f = id X )
assume A1: for x being Element of X holds f . x = x ; :: thesis: f = id X
let x be Element of X; :: according to FUNCT_2:def 9 :: thesis: f . x = (id X) . x
x = (id X) . x by FUNCT_1:35;
hence f . x = (id X) . x by A1; :: thesis: verum