let k be Element of 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 A1: ( 1 <= k & k < len sq ) ; :: thesis: (sq /^ 1) . k = sq . (k + 1)
then A2: len sq >= 1 by XXREAL_0:2;
then A3: len (sq /^ 1) = (len sq) - 1 by RFINSEQ:def 2;
A4: k + 1 <= len sq by A1, NAT_1:13;
len sq = ((len sq) - 1) + 1 ;
then k <= (len sq) - 1 by A4, XREAL_1:8;
then k in dom (sq /^ 1) by A1, A3, FINSEQ_3:27;
hence (sq /^ 1) . k = sq . (k + 1) by A2, RFINSEQ:def 2; :: thesis: verum