let v, v1 be FinSequence of REAL ; :: thesis: for n being Element of NAT st v is increasing & v1 = v | (Seg n) holds
v1 is increasing
let n be Element of NAT ; :: thesis: ( v is increasing & v1 = v | (Seg n) implies v1 is increasing )
assume that
A1: v is increasing and
A2: v1 = v | (Seg n) ; :: thesis: v1 is increasing

now

per cases ( n <= len v or len v <= n ) ;

suppose n <= len v ; :: thesis: v1 is increasing

then Seg n c= Seg (len v) by FINSEQ_1:7;
then A3: Seg n c= dom v by FINSEQ_1:def 3;
then Seg n = (dom v) /\ (Seg n) by XBOOLE_1:28;
then A4: dom v1 = Seg n by A2, RELAT_1:90;

now

let m, k be Element of NAT ; :: thesis: ( m in dom v1 & k in dom v1 & m < k implies v1 . m < v1 . k )
assume that
A5: ( m in dom v1 & k in dom v1 ) and
A6: m < k ; :: thesis: v1 . m < v1 . k
set r = v1 . m;
set s = v1 . k;
( v1 . m = v . m & v1 . k = v . k ) by A2, A5, FUNCT_1:70;
hence v1 . m < v1 . k by A1, A3, A4, A5, A6, SEQM_3:def 1; :: thesis: verum

end;

hence v1 is increasing by SEQM_3:def 1; :: thesis: verum

end;

suppose len v <= n ; :: thesis: v1 is increasing

hence v1 is increasing by A1, A2, FINSEQ_2:23; :: thesis: verum

end;

end;

end;

hence v1 is increasing ; :: thesis: verum