let D be non empty set ; :: thesis: for SD being Subset of D

for d being Element of D

for F being PartFunc of D,D st d in (dom F) /\ SD holds

F /. d = (F * (id SD)) /. d

let SD be Subset of D; :: thesis: for d being Element of D

for F being PartFunc of D,D st d in (dom F) /\ SD holds

F /. d = (F * (id SD)) /. d

let d be Element of D; :: thesis: for F being PartFunc of D,D st d in (dom F) /\ SD holds

F /. d = (F * (id SD)) /. d

let F be PartFunc of D,D; :: thesis: ( d in (dom F) /\ SD implies F /. d = (F * (id SD)) /. d )

assume A1: d in (dom F) /\ SD ; :: thesis: F /. d = (F * (id SD)) /. d

then A2: d in dom F by XBOOLE_0:def 4;

F . d = (F * (id SD)) . d by A1, FUNCT_1:20;

then A3: F /. d = (F * (id SD)) . d by A2, PARTFUN1:def 6;

A4: d in SD by A1, XBOOLE_0:def 4;

then A5: d in dom (id SD) by RELAT_1:45;

(id SD) /. d in dom F by A2, A4, Th6;

then d in dom (F * (id SD)) by A5, Th3;

hence F /. d = (F * (id SD)) /. d by A3, PARTFUN1:def 6; :: thesis: verum

for d being Element of D

for F being PartFunc of D,D st d in (dom F) /\ SD holds

F /. d = (F * (id SD)) /. d

let SD be Subset of D; :: thesis: for d being Element of D

for F being PartFunc of D,D st d in (dom F) /\ SD holds

F /. d = (F * (id SD)) /. d

let d be Element of D; :: thesis: for F being PartFunc of D,D st d in (dom F) /\ SD holds

F /. d = (F * (id SD)) /. d

let F be PartFunc of D,D; :: thesis: ( d in (dom F) /\ SD implies F /. d = (F * (id SD)) /. d )

assume A1: d in (dom F) /\ SD ; :: thesis: F /. d = (F * (id SD)) /. d

then A2: d in dom F by XBOOLE_0:def 4;

F . d = (F * (id SD)) . d by A1, FUNCT_1:20;

then A3: F /. d = (F * (id SD)) . d by A2, PARTFUN1:def 6;

A4: d in SD by A1, XBOOLE_0:def 4;

then A5: d in dom (id SD) by RELAT_1:45;

(id SD) /. d in dom F by A2, A4, Th6;

then d in dom (F * (id SD)) by A5, Th3;

hence F /. d = (F * (id SD)) /. d by A3, PARTFUN1:def 6; :: thesis: verum