let X, Y be non empty set ; :: 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
( max+ g = (max+ f) * (T ") & max- g = (max- f) * (T ") )
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
( max+ g = (max+ f) * (T ") & max- g = (max- f) * (T ") )
let f be PartFunc of X,ExtREAL; :: thesis: for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") holds
( max+ g = (max+ f) * (T ") & max- g = (max- f) * (T ") )
let g be PartFunc of Y,ExtREAL; :: thesis: ( T is bijective & g = f * (T ") implies ( max+ g = (max+ f) * (T ") & max- g = (max- f) * (T ") ) )
assume that
A1: T is bijective and
A2: g = f * (T ") ; :: thesis: ( max+ g = (max+ f) * (T ") & max- g = (max- f) * (T ") )
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 (max+ f) = dom f & dom (max- f) = dom f ) by MESFUNC2:def 2, MESFUNC2:def 3;
reconsider H = T " as Function of Y,X by A3, A4, FUNCT_2:1;
reconsider g1 = (max+ f) * H as PartFunc of Y,ExtREAL ;
A6: for x being object holds
( x in dom g1 iff x in dom g )

proof

let x be object ; :: thesis: ( x in dom g1 iff x in dom g )

hereby :: thesis: ( x in dom g implies x in dom g1 )

assume x in dom g1 ; :: thesis: x in dom g
then ( x in dom H & H . x in dom (max+ f) ) by FUNCT_1:11;
hence x in dom g by A2, A5, FUNCT_1:11; :: thesis: verum

end;

assume x in dom g ; :: thesis: x in dom g1
then ( x in dom H & H . x in dom f ) by A2, FUNCT_1:11;
hence x in dom g1 by FUNCT_1:11, A5; :: thesis: verum

end;

for y being Element of Y st y in dom g1 holds
g1 . y = max ((g . y),0.)

proof

let y be Element of Y; :: thesis: ( y in dom g1 implies g1 . y = max ((g . y),0.) )
assume y in dom g1 ; :: thesis: g1 . y = max ((g . y),0.)
then A7: ( y in dom H & H . y in dom (max+ f) ) by FUNCT_1:11;
reconsider x = H . y as Element of X ;
g1 . y = (max+ f) . x by FUNCT_1:13, A7;
then g1 . y = max ((f . x),0.) by A7, MESFUNC2:def 2;
hence g1 . y = max ((g . y),0.) by A2, A7, FUNCT_1:13; :: thesis: verum

end;

hence max+ g = (max+ f) * (T ") by A6, TARSKI:2, MESFUNC2:def 2; :: thesis: max- g = (max- f) * (T ")
reconsider g1 = (max- f) * H as PartFunc of Y,ExtREAL ;
A8: for x being object holds
( x in dom g1 iff x in dom g )

proof

let x be object ; :: thesis: ( x in dom g1 iff x in dom g )

hereby :: thesis: ( x in dom g implies x in dom g1 )

assume x in dom g1 ; :: thesis: x in dom g
then ( x in dom H & H . x in dom (max- f) ) by FUNCT_1:11;
hence x in dom g by A2, A5, FUNCT_1:11; :: thesis: verum

end;

assume x in dom g ; :: thesis: x in dom g1
then ( x in dom H & H . x in dom f ) by A2, FUNCT_1:11;
hence x in dom g1 by A5, FUNCT_1:11; :: thesis: verum

end;

for y being Element of Y st y in dom g1 holds
g1 . y = max ((- (g . y)),0.)

proof

let y be Element of Y; :: thesis: ( y in dom g1 implies g1 . y = max ((- (g . y)),0.) )
assume y in dom g1 ; :: thesis: g1 . y = max ((- (g . y)),0.)
then A9: ( y in dom H & H . y in dom (max- f) ) by FUNCT_1:11;
reconsider x = H . y as Element of X ;
g1 . y = (max- f) . x by FUNCT_1:13, A9;
then g1 . y = max ((- (f . x)),0.) by A9, MESFUNC2:def 3;
hence g1 . y = max ((- (g . y)),0.) by A2, A9, FUNCT_1:13; :: thesis: verum

end;

hence max- g = (max- f) * (T ") by A8, TARSKI:2, MESFUNC2:def 3; :: thesis: verum