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 Def19
.= s . x ; :: thesis: verum
end;
hence . x = . (^ x) by Def18; :: thesis: verum