let D be non empty set ; for f1 being FinSequence of D
for k being 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; for k being Nat st 1 <= k & k <= len f1 holds
( mid (f1,k,k) = <*(f1 /. k)*> & len (mid (f1,k,k)) = 1 )
let k be Nat; ( 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
; ( mid (f1,k,k) = <*(f1 /. k)*> & len (mid (f1,k,k)) = 1 )
A3:
f1 /. k = f1 . k
by A1, A2, FINSEQ_4:15;
(k -' 1) + 1 <= len f1
by A1, A2, XREAL_1:235;
then A4:
((k -' 1) + 1) - (k -' 1) <= (len f1) - (k -' 1)
by XREAL_1:9;
len (f1 /^ (k -' 1)) = (len f1) -' (k -' 1)
by RFINSEQ:29;
then A5:
1 <= len (f1 /^ (k -' 1))
by A4, NAT_D:39;
(k -' 1) + 1 = k
by A1, XREAL_1:235;
then A6:
(f1 /^ (k -' 1)) . 1 = f1 . k
by A2, FINSEQ_6:114;
(k -' k) + 1 =
(k - k) + 1
by XREAL_1:233
.=
1
;
then mid (f1,k,k) =
(f1 /^ (k -' 1)) | 1
by FINSEQ_6:def 3
.=
<*((f1 /^ (k -' 1)) . 1)*>
by A5, CARD_1:27, FINSEQ_5:20
;
hence
( mid (f1,k,k) = <*(f1 /. k)*> & len (mid (f1,k,k)) = 1 )
by A6, A3, FINSEQ_1:39; verum