let D be non empty set ; :: thesis: for f1 being FinSequence of D
for k being Element of NAT st 1 <= k & k <= len f1 holds
( mid f1,k,k = <*(f1 /. k)*> & len (mid f1,k,k) = 1 )
let f1 be FinSequence of D; :: thesis: for k being Element of NAT st 1 <= k & k <= len f1 holds
( mid f1,k,k = <*(f1 /. k)*> & len (mid f1,k,k) = 1 )
let k be Element of NAT ; :: thesis: ( 1 <= k & k <= len f1 implies ( mid f1,k,k = <*(f1 /. k)*> & len (mid f1,k,k) = 1 ) )
assume that
A1: 1 <= k and
A2: k <= len f1 ; :: thesis: ( mid f1,k,k = <*(f1 /. k)*> & len (mid f1,k,k) = 1 )
A3: f1 /. k = f1 . k by A1, A2, FINSEQ_4:24;
(k -' 1) + 1 <= len f1 by A1, A2, XREAL_1:237;
then A4: ((k -' 1) + 1) - (k -' 1) <= (len f1) - (k -' 1) by XREAL_1:11;
len (f1 /^ (k -' 1)) = (len f1) -' (k -' 1) by JORDAN3:19;
then A5: 1 <= len (f1 /^ (k -' 1)) by A4, NAT_D:39;
(k -' 1) + 1 = k by A1, XREAL_1:237;
then A6: (f1 /^ (k -' 1)) . 1 = f1 . k by A2, JORDAN3:23;
(k -' k) + 1 = (k - k) + 1 by XREAL_1:235
.= 1 ;
then mid f1,k,k = (f1 /^ (k -' 1)) | 1 by JORDAN3:def 1
.= <*((f1 /^ (k -' 1)) /. 1)*> by A5, CARD_1:47, FINSEQ_5:23 ;
hence ( mid f1,k,k = <*(f1 /. k)*> & len (mid f1,k,k) = 1 ) by A6, A3, A5, FINSEQ_1:56, FINSEQ_4:24; :: thesis: verum