let D be non empty set ; :: thesis: for f1 being FinSequence of D
for k being Nat st k < len f1 holds
( (f1 /^ k) . (len (f1 /^ k)) = f1 . (len f1) & (f1 /^ k) /. (len (f1 /^ k)) = f1 /. (len f1) )
let f1 be FinSequence of D; :: thesis: for k being Nat st k < len f1 holds
( (f1 /^ k) . (len (f1 /^ k)) = f1 . (len f1) & (f1 /^ k) /. (len (f1 /^ k)) = f1 /. (len f1) )
let k be Nat; :: thesis: ( k < len f1 implies ( (f1 /^ k) . (len (f1 /^ k)) = f1 . (len f1) & (f1 /^ k) /. (len (f1 /^ k)) = f1 /. (len f1) ) )
assume A1: k < len f1 ; :: thesis: ( (f1 /^ k) . (len (f1 /^ k)) = f1 . (len f1) & (f1 /^ k) /. (len (f1 /^ k)) = f1 /. (len f1) )
then k + 1 <= len f1 by NAT_1:13;
then (k + 1) - k <= (len f1) - k by XREAL_1:9;
then A2: 1 <= len (f1 /^ k) by A1, RFINSEQ:def 1;
then len (f1 /^ k) in Seg (len (f1 /^ k)) ;
then A3: len (f1 /^ k) in dom (f1 /^ k) by FINSEQ_1:def 3;
(len (f1 /^ k)) + k = ((len f1) - k) + k by A1, RFINSEQ:def 1
.= len f1 ;
hence A4: (f1 /^ k) . (len (f1 /^ k)) = f1 . (len f1) by A1, A3, RFINSEQ:def 1; :: thesis: (f1 /^ k) /. (len (f1 /^ k)) = f1 /. (len f1)
A5: (f1 /^ k) /. (len (f1 /^ k)) = (f1 /^ k) . (len (f1 /^ k)) by A2, FINSEQ_4:15;
0 + 1 <= len f1 by A1, NAT_1:13;
hence (f1 /^ k) /. (len (f1 /^ k)) = f1 /. (len f1) by A4, A5, FINSEQ_4:15; :: thesis: verum