let f1, f2 be PartFunc of X,ExtREAL; :: thesis: ( dom f1 = dom f & ( for x being Element of X st x in dom f1 holds
f1 . x = (f . x) |^ k ) & dom f2 = dom f & ( for x being Element of X st x in dom f2 holds
f2 . x = (f . x) |^ k ) implies f1 = f2 )
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: f1 = f2
for d being Element of X st d in dom f holds
f1 . d = f2 . d

proof

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

end;

hence f1 = f2 by A5, A7, PARTFUN1:5; :: thesis: verum