let X be non empty set ; :: thesis: for Y being non empty Subset of ExtREAL
for F being Function of X,Y holds rng (- F) = - (rng F)
let Y be non empty Subset of ExtREAL ; :: thesis: for F being Function of X,Y holds rng (- F) = - (rng F)
let F be Function of X,Y; :: thesis: rng (- F) = - (rng F)
thus rng (- F) c= - (rng F) :: according to XBOOLE_0:def 10 :: thesis: - (rng F) c= rng (- F)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (- F) or y in - (rng F) )
assume A1: y in rng (- F) ; :: thesis: y in - (rng F)
A2: dom F = X by FUNCT_2:def 1;
A3: ( dom (- F) = X & rng (- F) c= - Y ) by FUNCT_2:def 1, RELAT_1:def 19;
reconsider y = y as R_eal by A1;
consider a being set such that
A4: ( a in X & y = (- F) . a ) by A1, A3, FUNCT_1:def 5;
reconsider a = a as Element of X by A4;
( a in X & y = - (F . a) ) by A4, Def10;
then - y in rng F by A2, FUNCT_1:def 5;
then - (- y) in - (rng F) by Th23;
hence y in - (rng F) ; :: thesis: verum

end;

thus - (rng F) c= rng (- F) :: thesis: verum

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in - (rng F) or y in rng (- F) )
assume A5: y in - (rng F) ; :: thesis: y in rng (- F)
A6: dom (- F) = X by FUNCT_2:def 1;
A7: ( dom F = X & rng F c= Y ) by FUNCT_2:def 1, RELAT_1:def 19;
reconsider y = y as R_eal by A5;
- y in - (- (rng F)) by A5, Th23;
then - y in rng F by Th22;
then consider a being set such that
A8: ( a in X & - y = F . a ) by A7, FUNCT_1:def 5;
reconsider a = a as Element of X by A8;
y = - (F . a) by A8;
then y = (- F) . a by Def10;
hence y in rng (- F) by A6, FUNCT_1:def 5; :: thesis: verum

end;