let v, v1 be FinSequence of REAL ; :: thesis:
let n be Nat; :: thesis:
assume that
A1: v is increasing and
A2: v1 = v | (Seg n) ; :: thesis:

suppose n <= len v ; :: thesis:

then Seg n c= Seg (len v) by FINSEQ_1:5;
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:61;

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

end;

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

end;

suppose len v <= n ; :: thesis:

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

end;

end;

end;

hence v1 is increasing ; :: thesis: