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)

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

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) )
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;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

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