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