let D be non empty set ; :: thesis: for f being FinSequence of D
for n, m being Element of NAT st n <= m holds
len (f /^ m) <= len (f /^ n)
let f be FinSequence of D; :: thesis: for n, m being Element of NAT st n <= m holds
len (f /^ m) <= len (f /^ n)
let n, m be Element of NAT ; :: thesis: ( n <= m implies len (f /^ m) <= len (f /^ n) )
assume A1: n <= m ; :: thesis: len (f /^ m) <= len (f /^ n)
then A2: n - n <= m - n by XREAL_1:11;
A3: len (f /^ m) = (len f) -' m by JORDAN3:19;
then A4: (len (f /^ n)) - (len (f /^ m)) = ((len f) -' n) - ((len f) -' m) by JORDAN3:19;

now

per cases ( len f <= n or len f > n ) ;

suppose A5: len f <= n ; :: thesis: (len (f /^ n)) - (len (f /^ m)) >= 0

then ((len f) -' n) - ((len f) -' m) = ((len f) -' n) - 0 by A1, NAT_2:10, XXREAL_0:2
.= 0 by A5, NAT_2:10 ;
hence (len (f /^ n)) - (len (f /^ m)) >= 0 by A3, JORDAN3:19; :: thesis: verum

end;

suppose A6: len f > n ; :: thesis: (len (f /^ n)) - (len (f /^ m)) >= 0

per cases ( len f <= m or len f > m ) ;

suppose len f <= m ; :: thesis: (len (f /^ n)) - (len (f /^ m)) >= 0

then ((len f) -' n) - ((len f) -' m) = ((len f) -' n) - 0 by NAT_2:10
.= (len f) -' n ;
hence (len (f /^ n)) - (len (f /^ m)) >= 0 by A4; :: thesis: verum

end;

suppose len f > m ; :: thesis: (len (f /^ n)) - (len (f /^ m)) >= 0

then ((len f) -' n) - ((len f) -' m) = ((len f) -' n) - ((len f) - m) by XREAL_1:235
.= ((len f) - n) - ((len f) - m) by A6, XREAL_1:235
.= m - n ;
hence (len (f /^ n)) - (len (f /^ m)) >= 0 by A2, A3, JORDAN3:19; :: thesis: verum

end;

end;

end;

end;

end;

then ((len (f /^ n)) - (len (f /^ m))) + (len (f /^ m)) >= 0 + (len (f /^ m)) by XREAL_1:8;
hence len (f /^ m) <= len (f /^ n) ; :: thesis: verum