set V = R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A);

hereby :: thesis: ( not i = 1 implies m . (D . (i - 1)) is Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) )

assume i = 1 ; :: thesis: m . (lower_bound A) is Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A))
thus m . (lower_bound A) is Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) :: thesis: verum

proof

set f = m . (lower_bound A);
consider a, b being Real such that
A2: ( a <= b & A = [.a,b.] ) by MEASURE5:14;
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A3: lower_bound A = a by A2, INTEGRA1:5;
lower_bound A in A by A2, A3;
then m . (lower_bound A) in BoundedFunctions A by FUNCT_2:5;
hence m . (lower_bound A) is Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) by Lm1; :: thesis: verum

end;

end;

assume A5: i <> 1 ; :: thesis: m . (D . (i - 1)) is Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A))
set f = m . (D . (i - 1));
A6: ( 1 <= i & i <= (len D) + 1 ) by A1, FINSEQ_1:1;
then A7: i - 1 <= ((len D) + 1) - 1 by XREAL_1:9;
reconsider i1 = i - 1 as Nat by A6, INT_1:5, ORDINAL1:def 12;
1 < i by A5, A6, XXREAL_0:1;
then 1 - 1 < i1 by XREAL_1:14;
then 1 <= i1 by NAT_1:14;
then i - 1 in dom D by FINSEQ_3:25, A7;
then m . (D . (i - 1)) in BoundedFunctions A by FUNCT_2:5, INTEGRA1:6;
hence m . (D . (i - 1)) is Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) by Lm1; :: thesis: verum