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

now :: thesis: for x being object st x in eq_dom (f,a) holds
x in eq_dom (g,(a * r))

let x be object ; :: thesis: ( x in eq_dom (f,a) implies x in eq_dom (g,(a * r)) )
assume x in eq_dom (f,a) ; :: thesis: x in eq_dom (g,(a * r))
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: verum

end;

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

now :: thesis: for x being object st x in eq_dom (g,(a * r)) holds
x in eq_dom (f,a)

let x be object ; :: thesis: ( x in eq_dom (g,(a * r)) implies x in eq_dom (f,a) )
assume x in eq_dom (g,(a * r)) ; :: thesis: x in eq_dom (f,a)
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: verum

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: verum