let X, Y be set ; :: thesis: (id X) | Y = id (X /\ Y)
A1: ( dom (id (X \ Y)) = X \ Y & dom (id (X /\ Y)) = X /\ Y & (X \ Y) /\ (Y /\ Y) = {} & X /\ Y c= Y ) ;
then A2: ( dom (id (X \ Y)) misses Y & dom (id (X /\ Y)) c= Y ) ;
reconsider i = id (X /\ Y) as Y -defined Function by RELAT_1:def 18, A1;
X = (X /\ Y) \/ (X \ Y) ;
then id X = (id (X /\ Y)) \/ (id (X \ Y)) by SYSREL:14;
then (id X) | Y = ((id (X /\ Y)) | Y) \/ ((id (X \ Y)) | Y) by Th56;
then (id X) | Y = ((id (X /\ Y)) | Y) \/ {} by A2, RELAT_1:152
.= i null Y
.= i ;
hence (id X) | Y = id (X /\ Y) ; :: thesis: verum