let p1, p2, p3 be set ; :: thesis: <*p1,p2,p3*> | (Seg 2) = <*p1,p2*>
set f = <*p1,p2,p3*> | (Seg 2);
A1: len <*p1,p2,p3*> = 3 by FINSEQ_1:45;
then A2: 2 in dom <*p1,p2,p3*> by FINSEQ_3:25;
1 in dom <*p1,p2,p3*> by A1, FINSEQ_3:25;
then A3: Seg 2 c= dom <*p1,p2,p3*> by A2, FINSEQ_1:2, ZFMISC_1:32;
A4: dom (<*p1,p2,p3*> | (Seg 2)) = (dom <*p1,p2,p3*>) /\ (Seg 2) by RELAT_1:61
.= Seg 2 by A3, XBOOLE_1:28 ;
then reconsider f = <*p1,p2,p3*> | (Seg 2) as FinSequence by FINSEQ_1:def 2;
A5: len f = 2 by A4, FINSEQ_1:def 3;
then 2 in dom f by FINSEQ_3:25;
then A6: f . 2 = <*p1,p2,p3*> . 2 by FUNCT_1:47
.= p2 ;
1 in dom f by A5, FINSEQ_3:25;
then f . 1 = <*p1,p2,p3*> . 1 by FUNCT_1:47
.= p1 ;
hence <*p1,p2,p3*> | (Seg 2) = <*p1,p2*> by A5, A6, FINSEQ_1:44; :: thesis: verum