let X, Y be set ; :: thesis: (id X) * (id Y) = id (X /\ Y)
A1: dom ((id X) * (id Y)) = (dom (id X)) /\ Y by Th37
.= X /\ Y by Th34 ;
A2: X /\ Y = dom (id (X /\ Y)) by Th34;
for z being set st z in X /\ Y holds
((id X) * (id Y)) . z = (id (X /\ Y)) . z

proof

let z be set ; :: thesis: ( z in X /\ Y implies ((id X) * (id Y)) . z = (id (X /\ Y)) . z )
assume A3: z in X /\ Y ; :: thesis: ((id X) * (id Y)) . z = (id (X /\ Y)) . z
then A4: ( z in X & z in Y ) by XBOOLE_0:def 4;
thus ((id X) * (id Y)) . z = (id X) . ((id Y) . z) by A1, A3, Th22
.= (id X) . z by A4, Th34
.= z by A4, Th34
.= (id (X /\ Y)) . z by A3, Th34 ; :: thesis: verum

end;

hence (id X) * (id Y) = id (X /\ Y) by A1, A2, Th9; :: thesis: verum