let p be FinSequence; :: thesis: for x being object holds (<*x*> ^ p) . 1 = x
let x be object ; :: 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 ; :: thesis: verum