let X be non empty set ; :: thesis: for x being Element of X holds . x = . (^ x)
let x be Element of X; :: thesis: . x = . (^ x)
for s being Element of Funcs X,INT holds (. (^ x)) . s = s . x

proof

let s be Element of Funcs X,INT ; :: thesis: (. (^ x)) . s = s . x
thus (. (^ x)) . s = s . ((^ x) . s) by DEFvarexp
.= s . x by FUNCOP_1:13 ; :: thesis: verum

end;

hence . x = . (^ x) by DEFvarexp1; :: thesis: verum