let X be set ; :: thesis: for f being Function holds
( f = id X iff ( dom f = X & ( for x being object st x in X holds
f . x = x ) ) )
let f be Function; :: thesis: ( f = id X iff ( dom f = X & ( for x being object st x in X holds
f . x = x ) ) )

hereby :: thesis: ( dom f = X & ( for x being object st x in X holds
f . x = x ) implies f = id X )

assume A1: f = id X ; :: thesis: ( dom f = X & ( for x being object st x in X holds
f . x = x ) )
hence A2: dom f = X ; :: thesis: for x being object st x in X holds
f . x = x
let x be object ; :: thesis: ( x in X implies f . x = x )
assume A3: x in X ; :: thesis: f . x = x
then [x,x] in f by A1, RELAT_1:def 10;
hence f . x = x by A2, A3, Def2; :: thesis: verum

end;

assume that
A4: dom f = X and
A5: for x being object st x in X holds
f . x = x ; :: thesis: f = id X

now :: thesis: for x, y being object holds
( ( [x,y] in f implies ( x in X & x = y ) ) & ( x in X & x = y implies [x,y] in f ) )

let x, y be object ; :: thesis: ( ( [x,y] in f implies ( x in X & x = y ) ) & ( x in X & x = y implies [x,y] in f ) )

hereby :: thesis: ( x in X & x = y implies [x,y] in f )

assume A6: [x,y] in f ; :: thesis: ( x in X & x = y )
hence A7: x in X by A4, Th1; :: thesis: x = y
y = f . x by A6, Th1;
hence x = y by A5, A7; :: thesis: verum

end;

assume A8: x in X ; :: thesis: ( x = y implies [x,y] in f )
then f . x = x by A5;
hence ( x = y implies [x,y] in f ) by A4, A8, Th1; :: thesis: verum

end;

hence f = id X by RELAT_1:def 10; :: thesis: verum