let X be non empty set ; :: thesis:
let f, g be PartFunc of X,ExtREAL; :: thesis:
let a be ExtReal; :: thesis:
let r be Real; :: thesis:
assume that
A1: r <> 0 and
a2: g = r (#) f ; :: thesis:
A2: dom f = dom g by a2, MESFUNC1:def 6;

let x be object ; :: thesis:
assume x in eq_dom (f,a) ; :: thesis:
then ( x in dom f & f . x = a ) by MESFUNC1:def 15;
then ( x in dom g & g . x = r * a ) by a2, A2, MESFUNC1:def 6;
hence x in eq_dom (g,(a * r)) by MESFUNC1:def 15; :: thesis:

end;

then A3: eq_dom (f,a) c= eq_dom (g,(a * r)) ;

let x be object ; :: thesis:
assume x in eq_dom (g,(a * r)) ; :: thesis:
then A4: ( x in dom g & g . x = a * r ) by MESFUNC1:def 15;
then r * (f . x) = a * r by a2, MESFUNC1:def 6;
then f . x = a by A1, XXREAL_3:68;
hence x in eq_dom (f,a) by A2, A4, MESFUNC1:def 15; :: thesis:

end;

then eq_dom (g,(a * r)) c= eq_dom (f,a) ;
hence eq_dom (f,a) = eq_dom (g,(a * r)) by A3; :: thesis: