let D be non empty set ; :: thesis: for f being FinSequence of D
for k1, k2 being Element of NAT st 1 <= k1 & k1 <= k2 & k2 <= len f holds
len (mid f,k1,k2) <= len f
let f be FinSequence of D; :: thesis: for k1, k2 being Element of NAT st 1 <= k1 & k1 <= k2 & k2 <= len f holds
len (mid f,k1,k2) <= len f
let k1, k2 be Element of NAT ; :: thesis: ( 1 <= k1 & k1 <= k2 & k2 <= len f implies len (mid f,k1,k2) <= len f )
assume A1: ( 1 <= k1 & k1 <= k2 & k2 <= len f ) ; :: thesis: len (mid f,k1,k2) <= len f
then A2: 1 <= k2 by XXREAL_0:2;
k1 <= len f by A1, XXREAL_0:2;
then A3: len (mid f,k1,k2) = (k2 -' k1) + 1 by A1, A2, Th27;
k2 - k1 >= 0 by A1, XREAL_1:50;
then A4: (k2 -' k1) + 1 = (k2 - k1) + 1 by XREAL_0:def 2
.= k2 - (k1 - 1) ;
k1 - 1 >= 0 by A1, XREAL_1:50;
then A5: k1 - 1 = k1 -' 1 by XREAL_0:def 2;
k2 <= k2 + (k1 -' 1) by NAT_1:11;
then k2 - (k1 -' 1) <= (k2 + (k1 -' 1)) - (k1 -' 1) by XREAL_1:11;
hence len (mid f,k1,k2) <= len f by A1, A3, A4, A5, XXREAL_0:2; :: thesis: verum