let p1, p2, p3 be set ; :: thesis: <*p1,p2,p3*> | (Seg 1) = <*p1*>
set f = <*p1,p2,p3*> | (Seg 1);
len <*p1,p2,p3*> = 3 by FINSEQ_1:62;
then 1 in dom <*p1,p2,p3*> by FINSEQ_3:27;
then A1: Seg 1 c= dom <*p1,p2,p3*> by FINSEQ_1:4, ZFMISC_1:37;
A2: dom (<*p1,p2,p3*> | (Seg 1)) = (dom <*p1,p2,p3*>) /\ (Seg 1) by RELAT_1:90
.= Seg 1 by A1, XBOOLE_1:28 ;
then reconsider f = <*p1,p2,p3*> | (Seg 1) as FinSequence by FINSEQ_1:def 2;
1 in dom f by A2, FINSEQ_1:4, TARSKI:def 1;
then A3: f . 1 = <*p1,p2,p3*> . 1 by FUNCT_1:70
.= p1 by FINSEQ_1:62 ;
len f = 1 by A2, FINSEQ_1:def 3;
hence <*p1,p2,p3*> | (Seg 1) = <*p1*> by A3, FINSEQ_1:57; :: thesis: verum