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

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