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) )
A1: len (f /^ m) = (len f) -' m by RFINSEQ:29;
assume A2: n <= m ; :: thesis: len (f /^ m) <= len (f /^ n)
then A3: n - n <= m - n by XREAL_1:9;

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

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

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

then ((len f) -' n) - ((len f) -' m) = ((len f) -' n) - 0 by A2, NAT_2:8, XXREAL_0:2
.= 0 by A4, NAT_2:8 ;
hence (len (f /^ n)) - (len (f /^ m)) >= 0 by A1, RFINSEQ:29; :: thesis: verum

end;

suppose A5: 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:8
.= (len f) -' n ;
hence (len (f /^ n)) - (len (f /^ m)) >= 0 by A1; :: 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:233
.= ((len f) - n) - ((len f) - m) by A5, XREAL_1:233
.= m - n ;
hence (len (f /^ n)) - (len (f /^ m)) >= 0 by A3, A1, RFINSEQ:29; :: thesis: verum

end;

end;

end;

end;

end;

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