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 )

A4: dom F = SD and

A5: for d being Element of D st d in SD holds

F /. d = d ; :: thesis: F = id SD

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 that
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 A1, FUNCT_1:18;

hence F /. d = d by A2, A3, PARTFUN1:def 6; :: thesis: verum

end;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 A1, FUNCT_1:18;

hence F /. d = d by A2, A3, PARTFUN1:def 6; :: thesis: verum

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

hence
F = id SD
by A4, FUNCT_1:17; :: thesis: verumF . 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 A4, A6, PARTFUN1:def 6; :: thesis: verum

end;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 A4, A6, PARTFUN1:def 6; :: thesis: verum