let D be non empty set ; :: thesis: for p1 being Element of D
for f being FinSequence of D holds (<*p1*> ^ f) /^ 1 = f
let p1 be Element of D; :: thesis: for f being FinSequence of D holds (<*p1*> ^ f) /^ 1 = f
let f be FinSequence of D; :: thesis: (<*p1*> ^ f) /^ 1 = f
A1: (<*p1*> ^ f) /. 1 = p1 by FINSEQ_5:15;
1 in Seg 1 ;
then A2: 1 in dom <*p1*> by FINSEQ_1:38;
dom <*p1*> c= dom (<*p1*> ^ f) by FINSEQ_1:26;
then <*((<*p1*> ^ f) /. (0 + 1))*> ^ ((<*p1*> ^ f) /^ 1) = (<*p1*> ^ f) /^ 0 by A2, FINSEQ_5:31
.= <*p1*> ^ f ;
hence (<*p1*> ^ f) /^ 1 = f by A1, FINSEQ_1:33; :: thesis: verum