let D be non empty set ; :: thesis: for f1 being FinSequence of D
for k being Element of 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 Element of 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 Element of 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 A2: (k + 1) - k <= (len f1) - k by XREAL_1:11;
A3: 0 + 1 <= len f1 by A1, NAT_1:13;
A4: 1 <= len (f1 /^ k) by A1, A2, RFINSEQ:def 2;
then len (f1 /^ k) in Seg (len (f1 /^ k)) by FINSEQ_1:3;
then A5: ( len (f1 /^ k) in dom (f1 /^ k) & k <= len f1 ) by A1, FINSEQ_1:def 3;
(len (f1 /^ k)) + k = ((len f1) - k) + k by A1, RFINSEQ:def 2
.= len f1 ;
hence A6: (f1 /^ k) . (len (f1 /^ k)) = f1 . (len f1) by A5, RFINSEQ:def 2; :: thesis: (f1 /^ k) /. (len (f1 /^ k)) = f1 /. (len f1)
(f1 /^ k) /. (len (f1 /^ k)) = (f1 /^ k) . (len (f1 /^ k)) by A4, FINSEQ_4:24;
hence (f1 /^ k) /. (len (f1 /^ k)) = f1 /. (len f1) by A3, A6, FINSEQ_4:24; :: thesis: verum