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 A1: ( 1 <= k & k <= len f1 ) ; :: thesis: ( mid f1,k,k = <*(f1 /. k)*> & len (mid f1,k,k) = 1 )
A2: len (f1 /^ (k -' 1)) = (len f1) -' (k -' 1) by RFINSEQ:42;
(k -' 1) + 1 = k by A1, XREAL_1:237;
then A3: (f1 /^ (k -' 1)) . 1 = f1 . k by A1, Th23;
A4: f1 /. k = f1 . k by A1, FINSEQ_4:24;
(k -' 1) + 1 <= len f1 by A1, XREAL_1:237;
then ((k -' 1) + 1) - (k -' 1) <= (len f1) - (k -' 1) by XREAL_1:11;
then A5: ( 1 <= 1 & 1 <= len (f1 /^ (k -' 1)) ) by A2, NAT_D:39;
then A6: not f1 /^ (k -' 1) is empty by CARD_1:47;
(k -' k) + 1 = (k - k) + 1 by XREAL_1:235
.= 1 ;
then mid f1,k,k = (f1 /^ (k -' 1)) | 1 by Def1
.= <*((f1 /^ (k -' 1)) /. 1)*> by A6, FINSEQ_5:23 ;
hence ( mid f1,k,k = <*(f1 /. k)*> & len (mid f1,k,k) = 1 ) by A3, A4, A5, FINSEQ_1:56, FINSEQ_4:24; :: thesis: verum