let X, Y be non empty set ; :: thesis: for S being SigmaField of X
for T being Function of X,Y
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL
for A being Element of S st T is bijective & g = f * (T ") & A = dom f & f is A -measurable holds
ex B being Element of CopyField (T,S) st
( B = T .: A & B = dom g & g is B -measurable )
let S be SigmaField of X; :: thesis: for T being Function of X,Y
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL
for A being Element of S st T is bijective & g = f * (T ") & A = dom f & f is A -measurable holds
ex B being Element of CopyField (T,S) st
( B = T .: A & B = dom g & g is B -measurable )
let T be Function of X,Y; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL
for A being Element of S st T is bijective & g = f * (T ") & A = dom f & f is A -measurable holds
ex B being Element of CopyField (T,S) st
( B = T .: A & B = dom g & g is B -measurable )
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL
for A being Element of S st T is bijective & g = f * (T ") & A = dom f & f is A -measurable holds
ex B being Element of CopyField (T,S) st
( B = T .: A & B = dom g & g is B -measurable )
let f be PartFunc of X,ExtREAL; :: thesis: for g being PartFunc of Y,ExtREAL
for A being Element of S st T is bijective & g = f * (T ") & A = dom f & f is A -measurable holds
ex B being Element of CopyField (T,S) st
( B = T .: A & B = dom g & g is B -measurable )
let g be PartFunc of Y,ExtREAL; :: thesis: for A being Element of S st T is bijective & g = f * (T ") & A = dom f & f is A -measurable holds
ex B being Element of CopyField (T,S) st
( B = T .: A & B = dom g & g is B -measurable )
let A be Element of S; :: thesis: ( T is bijective & g = f * (T ") & A = dom f & f is A -measurable implies ex B being Element of CopyField (T,S) st
( B = T .: A & B = dom g & g is B -measurable ) )
assume that
A1: T is bijective and
A2: g = f * (T ") and
A3: A = dom f and
A4: f is A -measurable ; :: thesis: ex B being Element of CopyField (T,S) st
( B = T .: A & B = dom g & g is B -measurable )
dom (.: T) = bool X by FUNCT_2:def 1;
then (.: T) . A in (.: T) .: S by FUNCT_1:def 6;
then (.: T) . A in CopyField (T,S) by A1, Def2;
then reconsider B = T .: A as Element of CopyField (T,S) by A1, Th1;
take B ; :: thesis: ( B = T .: A & B = dom g & g is B -measurable )
dom g = (T ") " (dom f) by A2, RELAT_1:147;
hence ( B = T .: A & B = dom g & g is B -measurable ) by A3, A1, A2, A4, Th20, FUNCT_1:84; :: thesis: verum