let X be set ; :: thesis: for x, y being object st y in X holds
<:(X --> x),(id X):> . y = [x,y]
let x, y be object ; :: thesis: ( y in X implies <:(X --> x),(id X):> . y = [x,y] )
assume A1: y in X ; :: thesis: <:(X --> x),(id X):> . y = [x,y]
then y in dom <:(X --> x),(id X):> by Lm8;
hence <:(X --> x),(id X):> . y = [((X --> x) . y),((id X) . y)] by FUNCT_3:def 7
.= [x,((id X) . y)] by A1, FUNCOP_1:7
.= [x,y] by A1, FUNCT_1:18 ;
:: thesis: verum