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 B being Element of CopyField (T,S) st T is bijective & g = f * (T ") & B = dom g & g is B -measurable holds
ex A being Element of S st
( B = T .: A & A = dom f & f is A -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 B being Element of CopyField (T,S) st T is bijective & g = f * (T ") & B = dom g & g is B -measurable holds
ex A being Element of S st
( B = T .: A & A = dom f & f is A -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 B being Element of CopyField (T,S) st T is bijective & g = f * (T ") & B = dom g & g is B -measurable holds
ex A being Element of S st
( B = T .: A & A = dom f & f is A -measurable )
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL
for B being Element of CopyField (T,S) st T is bijective & g = f * (T ") & B = dom g & g is B -measurable holds
ex A being Element of S st
( B = T .: A & A = dom f & f is A -measurable )
let f be PartFunc of X,ExtREAL; :: thesis: for g being PartFunc of Y,ExtREAL
for B being Element of CopyField (T,S) st T is bijective & g = f * (T ") & B = dom g & g is B -measurable holds
ex A being Element of S st
( B = T .: A & A = dom f & f is A -measurable )
let g be PartFunc of Y,ExtREAL; :: thesis: for B being Element of CopyField (T,S) st T is bijective & g = f * (T ") & B = dom g & g is B -measurable holds
ex A being Element of S st
( B = T .: A & A = dom f & f is A -measurable )
let B be Element of CopyField (T,S); :: thesis: ( T is bijective & g = f * (T ") & B = dom g & g is B -measurable implies ex A being Element of S st
( B = T .: A & A = dom f & f is A -measurable ) )
assume that
A1: T is bijective and
A2: g = f * (T ") and
A3: B = dom g and
A4: g is B -measurable ; :: thesis: ex A being Element of S st
( B = T .: A & A = dom f & f is A -measurable )
consider H being Function of Y,X such that
A5: ( H is bijective & H = T " & H " = T & .: H = (.: T) " & (.: H) .: (CopyField (T,S)) = S & CopyField (H,(CopyField (T,S))) = S ) by A1, Th17;
T " B in S by Th19, A1;
then reconsider A = H .: B as Element of S by A5, FUNCT_1:85;
take A ; :: thesis: ( B = T .: A & A = dom f & f is A -measurable )
dom f in bool X ;
then A6: dom f in dom (.: T) by FUNCT_2:def 1;
.: T is bijective by A1, Th1;
then A7: rng (.: T) = bool Y by FUNCT_2:def 3;
H .: (dom g) = H .: ((.: T) . (dom f)) by A1, A2, Th15;
then A8: H .: (dom g) = (.: H) . ((.: T) . (dom f)) by A5, Th1;
T .: A = T .: ((.: H) . B) by A5, Th1;
then T .: A = (.: T) . ((.: H) . B) by A1, Th1;
then T .: A = B by A5, A7, FUNCT_1:35;
hence ( B = T .: A & A = dom f & f is A -measurable ) by A8, A1, A2, A4, A3, A6, A5, Th20, FUNCT_1:34; :: thesis: verum