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

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

let F be PartFunc of D,D; :: thesis: ( F = id SD iff ( dom F = SD & ( for d being Element of D st d in SD holds
F /. d = d ) ) )

thus ( F = id SD implies ( dom F = SD & ( for d being Element of D st d in SD holds
F /. d = d ) ) ) :: thesis: ( dom F = SD & ( for d being Element of D st d in SD holds
F /. d = d ) implies F = id SD )
proof
assume A1: F = id SD ; :: thesis: ( dom F = SD & ( for d being Element of D st d in SD holds
F /. d = d ) )

hence A2: dom F = SD by RELAT_1:45; :: thesis: for d being Element of D st d in SD holds
F /. d = d

let d be Element of D; :: thesis: ( d in SD implies F /. d = d )
assume A3: d in SD ; :: thesis: F /. d = d
then F . d = d by ;
hence F /. d = d by ; :: thesis: verum
end;
assume that
A4: dom F = SD and
A5: for d being Element of D st d in SD holds
F /. d = d ; :: thesis: F = id SD
now :: thesis: for x being object st x in SD holds
F . x = x
let x be object ; :: thesis: ( x in SD implies F . x = x )
assume A6: x in SD ; :: thesis: F . x = x
then reconsider x1 = x as Element of D ;
F /. x1 = x1 by A5, A6;
hence F . x = x by ; :: thesis: verum
end;
hence F = id SD by ; :: thesis: verum