let X be non empty set ; :: thesis: for f being PartFunc of X,REAL
for k being Real
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
for E being set holds (f | E) to_power k = (f to_power k) | E
let k be Real; :: 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
A1: dom ((f | E) to_power k) = dom (f | E) by MESFUN6C:def 4;
then dom ((f | E) to_power k) = (dom f) /\ E by RELAT_1:61;
then A2: dom ((f | E) to_power k) = (dom (f to_power k)) /\ E by MESFUN6C:def 4;
then A3: dom ((f | E) to_power k) = dom ((f to_power k) | E) by RELAT_1:61;

now :: thesis: for x being Element of X st x in dom ((f | E) to_power k) holds
((f | E) to_power k) . x = ((f to_power k) | E) . x

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 A4: 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 4;
then A5: ((f | E) to_power k) . x = (f . x) to_power k by A1, A4, FUNCT_1:47;
x in dom (f to_power k) by A2, A4, XBOOLE_0:def 4;
then ((f | E) to_power k) . x = (f to_power k) . x by A5, MESFUN6C:def 4;
hence ((f | E) to_power k) . x = ((f to_power k) | E) . x by A4, A3, FUNCT_1:47; :: thesis: verum

end;

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