let x, Y be set ; :: thesis: for f being Function holds
( x in dom ((id Y) * f) iff ( x in dom f & f . x in Y ) )
let f be Function; :: thesis: ( x in dom ((id Y) * f) iff ( x in dom f & f . x in Y ) )
dom (id Y) = Y by Th34;
hence ( x in dom ((id Y) * f) iff ( x in dom f & f . x in Y ) ) by Th21; :: thesis: verum