let x be set ; :: thesis: for p being FinSequence holds (<*x*> ^ p) . 1 = x
let p be FinSequence; :: thesis: (<*x*> ^ p) . 1 = x
1 in Seg 1 ;
then 1 in dom <*x*> by Def8;
then (<*x*> ^ p) . 1 = <*x*> . 1 by Def7;
hence (<*x*> ^ p) . 1 = x by Def8; :: thesis: verum