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 that
A1: 1 <= k1 and
A2: k1 <= k2 and
A3: k2 <= len f ; :: thesis: len (mid (f,k1,k2)) <= len f
A4: k1 <= len f by A2, A3, XXREAL_0:2;
k2 - k1 >= 0 by A2, XREAL_1:50;
then A5: (k2 -' k1) + 1 = (k2 - k1) + 1 by XREAL_0:def 2
.= k2 - (k1 - 1) ;
k2 <= k2 + (k1 -' 1) by NAT_1:11;
then A6: k2 - (k1 -' 1) <= (k2 + (k1 -' 1)) - (k1 -' 1) by XREAL_1:11;
k1 - 1 >= 0 by A1, XREAL_1:50;
then A7: k1 - 1 = k1 -' 1 by XREAL_0:def 2;
1 <= k2 by A1, A2, XXREAL_0:2;
then len (mid (f,k1,k2)) = (k2 -' k1) + 1 by A1, A2, A3, A4, Th27;
hence len (mid (f,k1,k2)) <= len f by A3, A5, A7, A6, XXREAL_0:2; :: thesis: verum