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:35;
then ( 1 <= (len f) + 1 & (len f) + 1 <= len (f ^ <*p*>) ) by FINSEQ_1:56, NAT_1:11;
then (len f) + 1 in dom (f ^ <*p*>) by FINSEQ_3:27;
hence (f ^ <*p*>) /. ((len f) + 1) = (f ^ <*p*>) . ((len f) + 1) by PARTFUN1:def 8
.= p by FINSEQ_1:59 ;
:: thesis: verum