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
( f is nonnegative iff g is nonnegative )
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 nonnegative iff g is nonnegative )
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 nonnegative iff g is nonnegative )
let g be PartFunc of Y,ExtREAL; :: thesis: ( T is bijective & g = f * (T ") implies ( f is nonnegative iff g is nonnegative ) )
assume A1: ( T is bijective & g = f * (T ") ) ; :: thesis: ( f is nonnegative iff g is nonnegative )
A2: dom T = X by FUNCT_2:def 1;
A3: 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 A4: g * T = f by RELAT_1:51, A2, A3;

hereby :: thesis: ( g is nonnegative implies f is nonnegative )

assume f is nonnegative ; :: thesis: g is nonnegative
then A5: rng f is nonnegative ;

now :: thesis: for y being ExtReal st y in rng g holds
0. <= y

let y be ExtReal; :: thesis: ( y in rng g implies 0. <= y )
assume y in rng g ; :: thesis: 0. <= y
then consider x being object such that
A6: ( x in dom g & y = g . x ) by FUNCT_1:def 3;
A7: y = f . ((T ") . x) by A1, A6, FUNCT_1:12;
( x in dom (T ") & (T ") . x in dom f ) by A1, A6, FUNCT_1:11;
hence 0. <= y by A5, A7, FUNCT_1:3; :: thesis: verum

end;

then rng g is nonnegative ;
hence g is nonnegative ; :: thesis: verum

end;

assume A8: g is nonnegative ; :: thesis: f is nonnegative

now :: thesis: for y being ExtReal st y in rng f holds
0. <= y

let y be ExtReal; :: thesis: ( y in rng f implies 0. <= y )
assume y in rng f ; :: thesis: 0. <= y
then consider x being object such that
A9: ( x in dom (g * T) & y = (g * T) . x ) by A4, FUNCT_1:def 3;
A10: ( x in dom T & T . x in dom g ) by A9, FUNCT_1:11;
y = g . (T . x) by FUNCT_1:12, A9;
hence 0. <= y by A8, A10, FUNCT_1:3, SUPINF_2:def 9; :: thesis: verum

end;

then rng f is nonnegative ;
hence f is nonnegative ; :: thesis: verum