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
A4: ( dom f1 = dom f & ( for d being Element of X st d in dom f1 holds
f1 . d = (f . d) |^ k ) ) and
A5: ( dom f2 = dom f & ( 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 d in dom f ; :: thesis: f1 . d = f2 . d
then ( f1 . d = (f . d) |^ k & f2 . d = (f . d) |^ k ) by A4, A5;
hence f1 . d = f2 . d ; :: thesis: verum

end;

hence f1 = f2 by A4, A5, PARTFUN1:34; :: thesis: verum