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;

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

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))

then A3:
eq_dom (f,a) c= eq_dom (g,(a * r))
;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;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

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

x in eq_dom (f,a)

then
eq_dom (g,(a * r)) c= eq_dom (f,a)
;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;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

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