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 d in dom ((id SD) * F) ; :: thesis: ( d in dom F & F /. d in SD )
then ( d in dom F & F /. d in dom (id SD) ) by Th6;
hence ( d in dom F & F /. d in SD ) by RELAT_1:71; :: thesis: verum

end;

assume ( d in dom F & F /. d in SD ) ; :: thesis: d in dom ((id SD) * F)
then ( d in dom F & F /. d in dom (id SD) ) by RELAT_1:71;
hence d in dom ((id SD) * F) by Th6; :: thesis: verum