let p be set ; :: thesis: p .. <*p*> = 1
A1: for i being Nat st 1 <= i & i < 1 holds
<*p*> . i <> <*p*> . 1 ;
dom <*p*> = Seg 1 by FINSEQ_1:38;
then A2: 1 in dom <*p*> by FINSEQ_1:2, TARSKI:def 1;
<*p*> . 1 = p by FINSEQ_1:40;
hence p .. <*p*> = 1 by A2, A1, Th4; :: thesis: verum