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