let f1, f2 be PartFunc of X,ExtREAL; :: thesis:
assume that
A5: dom f1 = dom f and
A6: for d being Element of X st d in dom f1 holds
f1 . d = (f . d) |^ k and
A7: dom f2 = dom f and
A8: for d being Element of X st d in dom f2 holds
f2 . d = (f . d) |^ k ; :: thesis:
for d being Element of X st d in dom f holds
f1 . d = f2 . d

let d be Element of X; :: thesis:
assume A9: d in dom f ; :: thesis:
then f1 . d = (f . d) |^ k by A5, A6;
hence f1 . d = f2 . d by A7, A8, A9; :: thesis:

end;