let x, X be set ; :: thesis: for f being Function st x in (dom f) /\ X holds
f . x = (f * (id X)) . x
let f be Function; :: thesis: ( x in (dom f) /\ X implies f . x = (f * (id X)) . x )
assume x in (dom f) /\ X ; :: thesis: f . x = (f * (id X)) . x
then ( dom (id X) = X & x in X & x in dom f ) by Th34, XBOOLE_0:def 4;
then ( (id X) . x = x & x in dom (id X) & x in dom f ) by Th34;
hence f . x = (f * (id X)) . x by Th23; :: thesis: verum