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

let x be Element of X; :: thesis: . x = . (^ x)

for s being Element of Funcs (X,INT) holds (. (^ x)) . s = s . x

proof

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

.= s . x ; :: thesis: verum