let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL holds
( f " {+infty} = (- f) " {-infty} & f " {-infty} = (- f) " {+infty} )
let f be PartFunc of X,ExtREAL; :: thesis: ( f " {+infty} = (- f) " {-infty} & f " {-infty} = (- f) " {+infty} )

now :: thesis: for x being set st x in f " {+infty} holds
x in (- f) " {-infty}

let x be set ; :: thesis: ( x in f " {+infty} implies x in (- f) " {-infty} )
assume x in f " {+infty} ; :: thesis: x in (- f) " {-infty}
then A1: ( x in dom f & f . x in {+infty} ) by FUNCT_1:def 7;
then A2: x in dom (- f) by MESFUNC1:def 7;
f . x = +infty by A1, TARSKI:def 1;
then (- f) . x = - +infty by A2, MESFUNC1:def 7;
then (- f) . x in {-infty} by XXREAL_3:6, TARSKI:def 1;
hence x in (- f) " {-infty} by A2, FUNCT_1:def 7; :: thesis: verum

end;

then A3: f " {+infty} c= (- f) " {-infty} ;

now :: thesis: for x being set st x in (- f) " {-infty} holds
x in f " {+infty}

let x be set ; :: thesis: ( x in (- f) " {-infty} implies x in f " {+infty} )
assume x in (- f) " {-infty} ; :: thesis: x in f " {+infty}
then A4: ( x in dom (- f) & (- f) . x in {-infty} ) by FUNCT_1:def 7;
then A5: x in dom f by MESFUNC1:def 7;
(- f) . x = -infty by A4, TARSKI:def 1;
then - (f . x) = -infty by A4, MESFUNC1:def 7;
then f . x in {+infty} by XXREAL_3:5, TARSKI:def 1;
hence x in f " {+infty} by A5, FUNCT_1:def 7; :: thesis: verum

end;

then (- f) " {-infty} c= f " {+infty} ;
hence f " {+infty} = (- f) " {-infty} by A3; :: thesis: f " {-infty} = (- f) " {+infty}

now :: thesis: for x being set st x in f " {-infty} holds
x in (- f) " {+infty}

let x be set ; :: thesis: ( x in f " {-infty} implies x in (- f) " {+infty} )
assume x in f " {-infty} ; :: thesis: x in (- f) " {+infty}
then A7: ( x in dom f & f . x in {-infty} ) by FUNCT_1:def 7;
then A8: x in dom (- f) by MESFUNC1:def 7;
f . x = -infty by A7, TARSKI:def 1;
then (- f) . x = - -infty by A8, MESFUNC1:def 7;
then (- f) . x in {+infty} by XXREAL_3:5, TARSKI:def 1;
hence x in (- f) " {+infty} by A8, FUNCT_1:def 7; :: thesis: verum

end;

then A9: f " {-infty} c= (- f) " {+infty} ;

now :: thesis: for x being set st x in (- f) " {+infty} holds
x in f " {-infty}

let x be set ; :: thesis: ( x in (- f) " {+infty} implies x in f " {-infty} )
assume x in (- f) " {+infty} ; :: thesis: x in f " {-infty}
then A10: ( x in dom (- f) & (- f) . x in {+infty} ) by FUNCT_1:def 7;
then A11: x in dom f by MESFUNC1:def 7;
(- f) . x = +infty by A10, TARSKI:def 1;
then - (f . x) = +infty by A10, MESFUNC1:def 7;
then f . x in {-infty} by XXREAL_3:6, TARSKI:def 1;
hence x in f " {-infty} by A11, FUNCT_1:def 7; :: thesis: verum

end;

then (- f) " {+infty} c= f " {-infty} ;
hence f " {-infty} = (- f) " {+infty} by A9; :: thesis: verum