theorem Th138: :: SEQ_4:139

for v, v1 being FinSequence of REAL
for n being Nat st v is increasing & v1 = v | (Seg n) holds
v1 is increasing