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 A1: ( x in dom (id X) & (id X) . x in dom f ) by Th21;
dom (id X) = X by Th34;
hence ( x in dom f & x in X ) by A1, Th34; :: thesis: verum

end;

assume A2: x in dom f ; :: thesis: ( not x in X or x in dom (f * (id X)) )
A3: dom (id X) = X by Th34;
assume A4: x in X ; :: thesis: x in dom (f * (id X))
then (id X) . x in dom f by A2, Th34;
hence x in dom (f * (id X)) by A4, A3, 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:1; :: thesis: verum