let X be non empty set ; :: thesis: for x being set holds the_value_of (X --> x) = x

let x be set ; :: thesis: the_value_of (X --> x) = x

set f = X --> x;

ex i being set st

( i in dom (X --> x) & the_value_of (X --> x) = (X --> x) . i ) by FUNCT_1:def 12;

hence the_value_of (X --> x) = x by Th7; :: thesis: verum

let x be set ; :: thesis: the_value_of (X --> x) = x

set f = X --> x;

ex i being set st

( i in dom (X --> x) & the_value_of (X --> x) = (X --> x) . i ) by FUNCT_1:def 12;

hence the_value_of (X --> x) = x by Th7; :: thesis: verum