let D be non empty set ; :: thesis: for f being FinSequence of D
for p being Element of D holds (f ^ <*p*>) /. ((len f) + 1) = p
let f be FinSequence of D; :: thesis: for p being Element of D holds (f ^ <*p*>) /. ((len f) + 1) = p
let p be Element of D; :: thesis: (f ^ <*p*>) /. ((len f) + 1) = p
len (f ^ <*p*>) = (len f) + (len <*p*>) by FINSEQ_1:22;
then ( 1 <= (len f) + 1 & (len f) + 1 <= len (f ^ <*p*>) ) by FINSEQ_1:39, NAT_1:11;
then (len f) + 1 in dom (f ^ <*p*>) by FINSEQ_3:25;
hence (f ^ <*p*>) /. ((len f) + 1) = (f ^ <*p*>) . ((len f) + 1) by PARTFUN1:def 6
.= p by FINSEQ_1:42 ;
:: thesis: verum