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 object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (- F) or y in - (rng F) )
A1: dom F = X by FUNCT_2:def 1;
assume A2: y in rng (- F) ; :: thesis: y in - (rng F)
then reconsider y = y as R_eal ;
dom (- F) = X by FUNCT_2:def 1;
then consider a being object such that
A3: a in X and
A4: y = (- F) . a by A2, FUNCT_1:def 3;
reconsider a = a as Element of X by A3;
y = - (F . a) by A4, Def4;
then - y in rng F by A1, FUNCT_1:def 3;
then - (- y) in - (rng F) ;
hence y in - (rng F) ; :: thesis: verum

end;

let y be object ; :: 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)
then reconsider y = y as R_eal ;
A6: - y in - (- (rng F)) by A5;
dom F = X by FUNCT_2:def 1;
then consider a being object such that
A7: a in X and
A8: - y = F . a by A6, FUNCT_1:def 3;
reconsider a = a as Element of X by A7;
y = - (F . a) by A8;
then A9: y = (- F) . a by Def4;
dom (- F) = X by FUNCT_2:def 1;
hence y in rng (- F) by A9, FUNCT_1:def 3; :: thesis: verum