let D be non empty set ; :: thesis:
let SD be Subset of D; :: thesis:
let F be PartFunc of D,D; :: thesis:
thus ( F = id SD implies ( dom F = SD & ( for d being Element of D st d in SD holds
F /. d = d ) ) ) :: thesis:

end;

assume that
A4: dom F = SD and
A5: for d being Element of D st d in SD holds
F /. d = d ; :: thesis:

let x be object ; :: thesis:
assume A6: x in SD ; :: thesis:
then reconsider x1 = x as Element of D ;
F /. x1 = x1 by A5, A6;
hence F . x = x by A4, A6, PARTFUN1:def 6; :: thesis:

end;