hereby :: thesis: ( ( for n being Nat st n in dom f holds
( r <= f . n & f . n <= s ) ) implies f lies_between r,s )

assume f lies_between r,s ; :: thesis: for n being Nat st n in dom f holds
( r <= f . n & f . n <= s )
then A1: rng f c= [.r,s.] ;
let n be Nat; :: thesis: ( n in dom f implies ( r <= f . n & f . n <= s ) )
assume n in dom f ; :: thesis: ( r <= f . n & f . n <= s )
then f . n in rng f by FUNCT_1:3;
hence ( r <= f . n & f . n <= s ) by A1, XXREAL_1:1; :: thesis: verum

end;

assume A2: for n being Nat st n in dom f holds
( r <= f . n & f . n <= s ) ; :: thesis: f lies_between r,s
let y be object ; :: according to TARSKI:def 3,GOBOARD4:def 1 :: thesis: ( not y in rng f or y in [.r,s.] )
assume y in rng f ; :: thesis: y in [.r,s.]
then consider x being object such that
A3: x in dom f and
A4: y = f . x by FUNCT_1:def 3;
reconsider n = x as Nat by A3;
( r <= f . n & f . n <= s ) by A2, A3;
hence y in [.r,s.] by A4, XXREAL_1:1; :: thesis: verum