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 st T is bijective & g = f * (T ") holds
( f is_simple_func_in S iff g is_simple_func_in CopyField (T,S) )
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 st T is bijective & g = f * (T ") holds
( f is_simple_func_in S iff g is_simple_func_in CopyField (T,S) )
let T be Function of X,Y; :: thesis: for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") holds
( f is_simple_func_in S iff g is_simple_func_in CopyField (T,S) )
let f be PartFunc of X,ExtREAL; :: thesis: for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") holds
( f is_simple_func_in S iff g is_simple_func_in CopyField (T,S) )
let g be PartFunc of Y,ExtREAL; :: thesis: ( T is bijective & g = f * (T ") implies ( f is_simple_func_in S iff g is_simple_func_in CopyField (T,S) ) )
assume A1: ( T is bijective & g = f * (T ") ) ; :: thesis: ( f is_simple_func_in S iff g is_simple_func_in CopyField (T,S) )
hence ( f is_simple_func_in S implies g is_simple_func_in CopyField (T,S) ) by Lm1; :: thesis: ( g is_simple_func_in CopyField (T,S) implies f is_simple_func_in S )
assume A2: g is_simple_func_in CopyField (T,S) ; :: thesis: f is_simple_func_in S
consider H being Function of Y,X such that
A3: ( H is bijective & H = T " & H " = T & .: H = (.: T) " & (.: H) .: (CopyField (T,S)) = S & CopyField (H,(CopyField (T,S))) = S ) by Th17, A1;
A4: dom T = X by FUNCT_2:def 1;
A5: dom f c= X ;
g * T = f * ((T ") * T) by A1, RELAT_1:36;
then g * T = f * (id (dom T)) by FUNCT_1:39, A1;
then g * T = f by RELAT_1:51, A4, A5;
hence f is_simple_func_in S by A2, A3, Lm1; :: thesis: verum