let X be non empty 1-sorted ; :: 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
for x being Element of X holds f . x = (id the carrier of X) . x

proof

let x be Element of X; :: thesis: f . x = (id the carrier of X) . x
x = (id the carrier of X) . x by FUNCT_1:35;
hence f . x = (id the carrier of X) . x by A1; :: thesis: verum

end;

hence f = id X by FUNCT_2:113; :: thesis: verum