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