let X be set ; :: thesis: for f being Function holds dom (f * (id X)) = (dom f) /\ X
let f be Function; :: thesis: dom (f * (id X)) = (dom f) /\ X
for x being set holds
( x in dom (f * (id X)) iff x in (dom f) /\ X )

proof

let x be set ; :: thesis: ( x in dom (f * (id X)) iff x in (dom f) /\ X )
( x in dom (f * (id X)) iff ( x in dom f & x in X ) )

proof

thus ( x in dom (f * (id X)) implies ( x in dom f & x in X ) ) :: thesis: ( x in dom f & x in X implies x in dom (f * (id X)) )

proof

assume x in dom (f * (id X)) ; :: thesis: ( x in dom f & x in X )
then ( x in dom (id X) & dom (id X) = X & (id X) . x in dom f ) by Th21, Th34;
hence ( x in dom f & x in X ) by Th34; :: thesis: verum

end;

assume A1: x in dom f ; :: thesis: ( not x in X or x in dom (f * (id X)) )
assume A2: x in X ; :: thesis: x in dom (f * (id X))
then ( (id X) . x in dom f & dom (id X) = X ) by A1, Th34;
hence x in dom (f * (id X)) by A2, Th21; :: thesis: verum

end;

hence ( x in dom (f * (id X)) iff x in (dom f) /\ X ) by XBOOLE_0:def 4; :: thesis: verum

end;

hence dom (f * (id X)) = (dom f) /\ X by TARSKI:2; :: thesis: verum