let k be Nat; for f1 being FinSequence st k in dom f1 holds
( mid (f1,k,k) = <*(f1 . k)*> & len (mid (f1,k,k)) = 1 )
let f1 be FinSequence; ( k in dom f1 implies ( mid (f1,k,k) = <*(f1 . k)*> & len (mid (f1,k,k)) = 1 ) )
assume A0:
k in dom f1
; ( mid (f1,k,k) = <*(f1 . k)*> & len (mid (f1,k,k)) = 1 )
then A1:
1 <= k
by FINSEQ_3:25;
A2:
k <= len f1
by A0, FINSEQ_3:25;
(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, FINSEQ_1:39; verum