let X be non empty set ; :: thesis: for f being PartFunc of X,REAL holds f to_power 1 = f
let f be PartFunc of X,REAL ; :: thesis: f to_power 1 = f
A1: dom (f to_power 1) = dom f by MESFUN6C:def 6;
for x being set st x in dom (f to_power 1) holds
(f to_power 1) . x = f . x

proof

let x be set ; :: thesis: ( x in dom (f to_power 1) implies (f to_power 1) . x = f . x )
assume x in dom (f to_power 1) ; :: thesis: (f to_power 1) . x = f . x
then (f to_power 1) . x = (f . x) to_power 1 by MESFUN6C:def 6;
hence (f to_power 1) . x = f . x by POWER:30; :: thesis: verum

end;

hence f to_power 1 = f by A1, FUNCT_1:9; :: thesis: verum