let k be Nat; :: thesis: for D being non empty set
for sq being FinSequence of D st 1 <= k & k < len sq holds
(sq /^ 1) . k = sq . (k + 1)
let D be non empty set ; :: thesis: for sq being FinSequence of D st 1 <= k & k < len sq holds
(sq /^ 1) . k = sq . (k + 1)
let sq be FinSequence of D; :: thesis: ( 1 <= k & k < len sq implies (sq /^ 1) . k = sq . (k + 1) )
assume that
A1: 1 <= k and
A2: k < len sq ; :: thesis: (sq /^ 1) . k = sq . (k + 1)
A3: len sq = ((len sq) - 1) + 1 ;
k + 1 <= len sq by A2, NAT_1:13;
then A4: k <= (len sq) - 1 by A3, XREAL_1:6;
A5: len sq >= 1 by A1, A2, XXREAL_0:2;
then len (sq /^ 1) = (len sq) - 1 by RFINSEQ:def 1;
then k in dom (sq /^ 1) by A1, A4, FINSEQ_3:25;
hence (sq /^ 1) . k = sq . (k + 1) by A5, RFINSEQ:def 1; :: thesis: verum