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) )

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

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 that
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;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

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