let X be set ; :: thesis: for x being object
for f being Function st x in (dom f) /\ X holds
f . x = (f * (id X)) . x
let x be object ; :: 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 x in X by XBOOLE_0:def 4;
then ( (id X) . x = x & x in dom (id X) ) by Th17;
hence f . x = (f * (id X)) . x by Th13; :: thesis: verum