let Y be set ; :: thesis: for x being object
for f being Function holds
( x in dom ((id Y) * f) iff ( x in dom f & f . x in Y ) )
let x be object ; :: 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 ;
hence ( x in dom ((id Y) * f) iff ( x in dom f & f . x in Y ) ) by Th11; :: thesis: verum