let p be increasing FinSequence of REAL ; :: thesis: for i, j being Element of NAT st j in dom p & i <= j holds
mid (p,i,j) is increasing FinSequence of REAL
let i, j be Element of NAT ; :: thesis: ( j in dom p & i <= j implies mid (p,i,j) is increasing FinSequence of REAL )
assume that
A1: j in dom p and
A2: i <= j ; :: thesis: mid (p,i,j) is increasing FinSequence of REAL
j in Seg (len p) by A1, FINSEQ_1:def 3;
then j <= len p by FINSEQ_1:1;
then i <= len p by A2, XXREAL_0:2;
then p /^ (i -' 1) is increasing FinSequence of REAL by Th32, NAT_D:44;
then A3: (p /^ (i -' 1)) | (Seg ((j -' i) + 1)) is increasing FinSequence of REAL by FINSEQ_1:18;
mid (p,i,j) = (p /^ (i -' 1)) | ((j -' i) + 1) by A2, FINSEQ_6:def 3;
hence mid (p,i,j) is increasing FinSequence of REAL by A3, FINSEQ_1:def 16; :: thesis: verum