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