let X be non empty set ; 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; 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; for r being Real st r <> 0 & g = r (#) f holds
eq_dom (f,a) = eq_dom (g,(a * r))
let r be Real; ( 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
; eq_dom (f,a) = eq_dom (g,(a * r))
A2:
dom f = dom g
by a2, MESFUNC1:def 6;
then A3:
eq_dom (f,a) c= eq_dom (g,(a * r))
;
then
eq_dom (g,(a * r)) c= eq_dom (f,a)
;
hence
eq_dom (f,a) = eq_dom (g,(a * r))
by A3; verum