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 & d in SD ) by XBOOLE_0:def 4;
then A3: (id SD) /. d in dom F by Th12;
d in dom (id SD) by A2, RELAT_1:71;
then A4: d in dom (F * (id SD)) by A3, Th6;
F . d = (F * (id SD)) . d by A1, FUNCT_1:38;
then F /. d = (F * (id SD)) . d by A2, PARTFUN1:def 8;
hence F /. d = (F * (id SD)) /. d by A4, PARTFUN1:def 8; :: thesis: verum