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;
A2: 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 A3: x in dom (1 (#) f) ; :: thesis: f . x = (1 (#) f) . x
A4: (1 (#) f) . x = (R_EAL 1) * (f . x) by A3, MESFUNC1:def 6;
thus f . x = (1 (#) f) . x by A4, XXREAL_3:92; :: thesis: verum

end;

thus f = 1 (#) f by A1, A2, PARTFUN1:34; :: thesis: verum