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 holds
( d in dom ((id SD) * F) iff ( d in dom F & F /. d in SD ) )
let SD be Subset of D; :: thesis: for d being Element of D
for F being PartFunc of D,D holds
( d in dom ((id SD) * F) iff ( d in dom F & F /. d in SD ) )
let d be Element of D; :: thesis: for F being PartFunc of D,D holds
( d in dom ((id SD) * F) iff ( d in dom F & F /. d in SD ) )
let F be PartFunc of D,D; :: thesis: ( d in dom ((id SD) * F) iff ( d in dom F & F /. d in SD ) )
thus ( d in dom ((id SD) * F) implies ( d in dom F & F /. d in SD ) ) :: thesis: ( d in dom F & F /. d in SD implies d in dom ((id SD) * F) )

proof

assume A1: d in dom ((id SD) * F) ; :: thesis: ( d in dom F & F /. d in SD )
then F /. d in dom (id SD) by Th3;
hence ( d in dom F & F /. d in SD ) by A1, Th3, RELAT_1:45; :: thesis: verum

end;

assume that
A2: d in dom F and
A3: F /. d in SD ; :: thesis: d in dom ((id SD) * F)
F /. d in dom (id SD) by A3, RELAT_1:45;
hence d in dom ((id SD) * F) by A2, Th3; :: thesis: verum