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:45;
then 1 in dom <*p1,p2,p3*> by FINSEQ_3:25;
then A1: Seg 1 c= dom <*p1,p2,p3*> by FINSEQ_1:2, ZFMISC_1:31;
A2: dom (<*p1,p2,p3*> | (Seg 1)) = (dom <*p1,p2,p3*>) /\ (Seg 1) by RELAT_1:61
.= 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;
then A3: f . 1 = <*p1,p2,p3*> . 1 by FUNCT_1:47
.= p1 by FINSEQ_1:45 ;
len f = 1 by A2, FINSEQ_1:def 3;
hence <*p1,p2,p3*> | (Seg 1) = <*p1*> by A3, FINSEQ_1:40; :: thesis: verum