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 A1: ( v is increasing & 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 A2: Seg n c= dom v by FINSEQ_1:def 3;
then Seg n = (dom v) /\ (Seg n) by XBOOLE_1:28;
then A3: dom v1 = Seg n by A1, 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 A4: ( m in dom v1 & k in dom v1 & m < k ) ; :: thesis: v1 . m < v1 . k
set r = v1 . m;
set s = v1 . k;
( v1 . m = v . m & v1 . k = v . k & m in dom v & k in dom v ) by A1, A2, A3, A4, FUNCT_1:70;
hence v1 . m < v1 . k by A1, A4, 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, FINSEQ_2:23; :: thesis: verum

end;

end;

end;

hence v1 is increasing ; :: thesis: verum