let X be set ; :: thesis: for x being object holds rng <:(X --> x),(id X):> = [:{x},X:]
let x be object ; :: thesis: rng <:(X --> x),(id X):> = [:{x},X:]

now :: thesis: for y being object holds
( ( y in [:{x},X:] implies ex x9 being object st
( x9 in dom <:(X --> x),(id X):> & y = <:(X --> x),(id X):> . x9 ) ) & ( ex x9 being object st
( x9 in dom <:(X --> x),(id X):> & y = <:(X --> x),(id X):> . x9 ) implies y in [:{x},X:] ) )

let y be object ; :: thesis: ( ( y in [:{x},X:] implies ex x9 being object st
( x9 in dom <:(X --> x),(id X):> & y = <:(X --> x),(id X):> . x9 ) ) & ( ex x9 being object st
( x9 in dom <:(X --> x),(id X):> & y = <:(X --> x),(id X):> . x9 ) implies y in [:{x},X:] ) )

hereby :: thesis: ( ex x9 being object st
( x9 in dom <:(X --> x),(id X):> & y = <:(X --> x),(id X):> . x9 ) implies y in [:{x},X:] )

assume y in [:{x},X:] ; :: thesis: ex x9 being object st
( x9 in dom <:(X --> x),(id X):> & y = <:(X --> x),(id X):> . x9 )
then consider x0, x9 being object such that
A1: ( x0 in {x} & x9 in X & y = [x0,x9] ) by ZFMISC_1:def 2;
take x9 = x9; :: thesis: ( x9 in dom <:(X --> x),(id X):> & y = <:(X --> x),(id X):> . x9 )
thus x9 in dom <:(X --> x),(id X):> by A1, Lm8; :: thesis: y = <:(X --> x),(id X):> . x9
thus y = [x,x9] by A1, TARSKI:def 1
.= <:(X --> x),(id X):> . x9 by A1, Lm9 ; :: thesis: verum

end;

given x9 being object such that A2: ( x9 in dom <:(X --> x),(id X):> & y = <:(X --> x),(id X):> . x9 ) ; :: thesis: y in [:{x},X:]
A3: x9 in X by A2, Lm8;
then y = [x,x9] by A2, Lm9;
hence y in [:{x},X:] by A3, ZFMISC_1:105; :: thesis: verum

end;

hence rng <:(X --> x),(id X):> = [:{x},X:] by FUNCT_1:def 3; :: thesis: verum