let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL holds f = 1 (#) f
let f be PartFunc of X,ExtREAL; :: thesis: f = 1 (#) f
A1: dom f = dom (1 (#) f) by MESFUNC1:def 6;
for x being Element of X st x in dom (1 (#) f) holds
f . x = (1 (#) f) . x

proof

let x be Element of X; :: thesis: ( x in dom (1 (#) f) implies f . x = (1 (#) f) . x )
assume x in dom (1 (#) f) ; :: thesis: f . x = (1 (#) f) . x
then (1 (#) f) . x = 1 * (f . x) by MESFUNC1:def 6;
hence f . x = (1 (#) f) . x by XXREAL_3:81; :: thesis: verum

end;

hence f = 1 (#) f by A1, PARTFUN1:5; :: thesis: verum