let X be non empty set ; :: thesis: for f being PartFunc of X,REAL
for k being real number
for E being set holds (f | E) to_power k = (f to_power k) | E
let f be PartFunc of X,REAL; :: thesis: for k being real number
for E being set holds (f | E) to_power k = (f to_power k) | E
let k be real number ; :: thesis: for E being set holds (f | E) to_power k = (f to_power k) | E
let E be set ; :: thesis: (f | E) to_power k = (f to_power k) | E
B1: dom ((f | E) to_power k) = dom (f | E) by MESFUN6C:def 6;
then dom ((f | E) to_power k) = (dom f) /\ E by RELAT_1:90;
then B3: dom ((f | E) to_power k) = (dom (f to_power k)) /\ E by MESFUN6C:def 6;
then A1: dom ((f | E) to_power k) = dom ((f to_power k) | E) by RELAT_1:90;

now

let x be Element of X; :: thesis: ( x in dom ((f | E) to_power k) implies ((f | E) to_power k) . x = ((f to_power k) | E) . x )
assume B2: x in dom ((f | E) to_power k) ; :: thesis: ((f | E) to_power k) . x = ((f to_power k) | E) . x
then ((f | E) to_power k) . x = ((f | E) . x) to_power k by MESFUN6C:def 6;
then B5: ((f | E) to_power k) . x = (f . x) to_power k by B1, B2, FUNCT_1:70;
x in dom (f to_power k) by B3, B2, XBOOLE_0:def 4;
then ((f | E) to_power k) . x = (f to_power k) . x by B5, MESFUN6C:def 6;
hence ((f | E) to_power k) . x = ((f to_power k) | E) . x by B2, A1, FUNCT_1:70; :: thesis: verum

end;

hence (f | E) to_power k = (f to_power k) | E by A1, PARTFUN1:34; :: thesis: verum