let X, Y be non empty set ; :: thesis: for S being SigmaField of X
for T being Function of X,Y
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL
for A being Element of S
for B being Element of CopyField (T,S) st T is bijective & g = f * (T ") holds
for r being Real holds T .: (less_dom (f,r)) = less_dom (g,r)
let S be SigmaField of X; :: thesis: for T being Function of X,Y
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL
for A being Element of S
for B being Element of CopyField (T,S) st T is bijective & g = f * (T ") holds
for r being Real holds T .: (less_dom (f,r)) = less_dom (g,r)
let T be Function of X,Y; :: thesis: for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL
for A being Element of S
for B being Element of CopyField (T,S) st T is bijective & g = f * (T ") holds
for r being Real holds T .: (less_dom (f,r)) = less_dom (g,r)
let f be PartFunc of X,ExtREAL; :: thesis: for g being PartFunc of Y,ExtREAL
for A being Element of S
for B being Element of CopyField (T,S) st T is bijective & g = f * (T ") holds
for r being Real holds T .: (less_dom (f,r)) = less_dom (g,r)
let g be PartFunc of Y,ExtREAL; :: thesis: for A being Element of S
for B being Element of CopyField (T,S) st T is bijective & g = f * (T ") holds
for r being Real holds T .: (less_dom (f,r)) = less_dom (g,r)
let A be Element of S; :: thesis: for B being Element of CopyField (T,S) st T is bijective & g = f * (T ") holds
for r being Real holds T .: (less_dom (f,r)) = less_dom (g,r)
let B be Element of CopyField (T,S); :: thesis: ( T is bijective & g = f * (T ") implies for r being Real holds T .: (less_dom (f,r)) = less_dom (g,r) )
assume that
A1: T is bijective and
A2: g = f * (T ") ; :: thesis: for r being Real holds T .: (less_dom (f,r)) = less_dom (g,r)
A3: ( dom T = X & rng T = Y ) by A1, FUNCT_2:def 1, FUNCT_2:def 3;
A4: ( rng T = dom (T ") & dom T = rng (T ") ) by A1, FUNCT_1:33;
A5: ( dom f c= X & rng f c= ExtREAL ) ;
g * T = f * ((T ") * T) by A2, RELAT_1:36;
then g * T = f * (id (dom T)) by A1, FUNCT_1:39;
then A6: g * T = f by A3, A5, RELAT_1:51;
let r be Real; :: thesis: T .: (less_dom (f,r)) = less_dom (g,r)
for x being object holds
( x in T .: (less_dom (f,r)) iff x in less_dom (g,r) )

proof

let x be object ; :: thesis: ( x in T .: (less_dom (f,r)) iff x in less_dom (g,r) )

hereby :: thesis: ( x in less_dom (g,r) implies x in T .: (less_dom (f,r)) )

assume x in T .: (less_dom (f,r)) ; :: thesis: x in less_dom (g,r)
then consider t being object such that
A7: ( t in dom T & t in less_dom (f,r) & x = T . t ) by FUNCT_1:def 6;
A8: ( t in dom f & f . t < r ) by A7, MESFUNC1:def 11;
A9: g . (T . t) = f . t by A6, A7, FUNCT_1:13;
T . t in dom g by A8, A6, FUNCT_1:11;
hence x in less_dom (g,r) by A7, A8, A9, MESFUNC1:def 11; :: thesis: verum

end;

assume A10: x in less_dom (g,r) ; :: thesis: x in T .: (less_dom (f,r))
then ( x in dom g & g . x < r ) by MESFUNC1:def 11;
then ( (T ") . x in dom f & f . ((T ") . x) < r ) by A3, A4, A2, FUNCT_1:11, FUNCT_1:13;
then A11: (T ") . x in less_dom (f,r) by MESFUNC1:def 11;
x = T . ((T ") . x) by A1, A10, FUNCT_1:35, A3;
hence x in T .: (less_dom (f,r)) by A11, A3, FUNCT_1:def 6; :: thesis: verum

end;

hence T .: (less_dom (f,r)) = less_dom (g,r) by TARSKI:2; :: thesis: verum