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

proof

let z be object ; :: 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 by XBOOLE_0:def 4;
A5: z in Y by A3, XBOOLE_0:def 4;
thus ((id X) * (id Y)) . z = (id X) . ((id Y) . z) by A1, A3, Th12
.= (id X) . z by A5, Th17
.= z by A4, Th17
.= (id (X /\ Y)) . z by A3, Th17 ; :: thesis: verum

end;

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