let r be Real; :: thesis: for p being FinSequence of REAL st ( for i being Nat st i in dom p holds
r <= p . i ) & ex i0 being Nat st
( i0 in dom p & p . i0 = r ) holds
r = inf (rng p)
let p be FinSequence of REAL ; :: thesis: ( ( for i being Nat st i in dom p holds
r <= p . i ) & ex i0 being Nat st
( i0 in dom p & p . i0 = r ) implies r = inf (rng p) )
assume that
A1: for i being Nat st i in dom p holds
r <= p . i and
A2: ex i0 being Nat st
( i0 in dom p & p . i0 = r ) ; :: thesis: r = inf (rng p)
set X = rng p;
consider i0 being Nat such that
A3: i0 in dom p and
A4: p . i0 = r by A2;
reconsider X = rng p as non empty real-membered bounded_below set by A3, A4, FUNCT_1:def 3;
A5: for a being Real st a in X holds
r <= a
proof
let a be Real; :: thesis: ( a in X implies r <= a )
assume a in X ; :: thesis: r <= a
then ex i being object st
( i in dom p & p . i = a ) by FUNCT_1:def 3;
hence r <= a by A1; :: thesis: verum
end;
for s being Real st 0 < s holds
ex a being Real st
( a in X & a < r + s )
proof
let s be Real; :: thesis: ( 0 < s implies ex a being Real st
( a in X & a < r + s ) )
assume A6: 0 < s ; :: thesis: ex a being Real st
( a in X & a < r + s )
consider i0 being Nat such that
A7: i0 in dom p and
A8: p . i0 = r by A2;
reconsider a = p . i0 as Real ;
take a ; :: thesis: ( a in X & a < r + s )
thus a in X by A7, FUNCT_1:def 3; :: thesis: a < r + s
r + 0 < r + s by A6, XREAL_1:8;
hence a < r + s by A8; :: thesis: verum
end;
then r = lower_bound X by A5, SEQ_4:def 2;
hence r = inf (rng p) ; :: thesis: verum