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 4;
for x being object st x in dom (f to_power 1) holds
(f to_power 1) . x = f . x

proof

let x be object ; :: 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 4;
hence (f to_power 1) . x = f . x by POWER:25; :: thesis: verum

end;

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