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:3;
then i <= len p by A2, XXREAL_0:2;
then p /^ (i -' 1) is increasing FinSequence of REAL by Th36, NAT_D:44;
then A3: (p /^ (i -' 1)) | (Seg ((j -' i) + 1)) is increasing FinSequence of REAL by FINSEQ_1:23, GOBOARD2:20;
mid p,i,j = (p /^ (i -' 1)) | ((j -' i) + 1) by A2, JORDAN3:def 1;
hence mid p,i,j is increasing FinSequence of REAL by A3, FINSEQ_1:def 15; :: thesis: verum