let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A
for m being Function of A,(BoundedFunctions A)
for rho being Function of A,REAL ex s being FinSequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st
( len s = len D & ( for i being Nat st i in dom s holds
s . i = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i))) ) )
let D be Division of A; :: thesis: for m being Function of A,(BoundedFunctions A)
for rho being Function of A,REAL ex s being FinSequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st
( len s = len D & ( for i being Nat st i in dom s holds
s . i = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i))) ) )
let m be Function of A,(BoundedFunctions A); :: thesis: for rho being Function of A,REAL ex s being FinSequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st
( len s = len D & ( for i being Nat st i in dom s holds
s . i = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i))) ) )
let rho be Function of A,REAL; :: thesis: ex s being FinSequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st
( len s = len D & ( for i being Nat st i in dom s holds
s . i = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i))) ) )
set V = R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A);
defpred S₁[ Nat, set ] means $2 = (sgn ((Dp2 (rho,D,($1 + 1))) - (Dp2 (rho,D,$1)))) * ((Dp1 (m,D,($1 + 1))) - (Dp1 (m,D,$1)));
A0: for i being Nat st i in Seg (len D) holds
ex x being Element of the carrier of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) st S₁[i,x] ;
consider s being FinSequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) such that
A1: ( dom s = Seg (len D) & ( for i being Nat st i in Seg (len D) holds
S₁[i,s . i] ) ) from FINSEQ_1:sch 5(A0);
take s ; :: thesis: ( len s = len D & ( for i being Nat st i in dom s holds
s . i = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i))) ) )
thus ( len s = len D & ( for i being Nat st i in dom s holds
s . i = (sgn ((Dp2 (rho,D,(i + 1))) - (Dp2 (rho,D,i)))) * ((Dp1 (m,D,(i + 1))) - (Dp1 (m,D,i))) ) ) by A1, FINSEQ_1:def 3; :: thesis: verum