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 by FINSEQ_1:45 ;

1 in dom f by A5, FINSEQ_3:25;

then f . 1 = <*p1,p2,p3*> . 1 by FUNCT_1:47

.= p1 by FINSEQ_1:45 ;

hence <*p1,p2,p3*> | (Seg 2) = <*p1,p2*> by A5, A6, FINSEQ_1:44; :: thesis: verum

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 by FINSEQ_1:45 ;

1 in dom f by A5, FINSEQ_3:25;

then f . 1 = <*p1,p2,p3*> . 1 by FUNCT_1:47

.= p1 by FINSEQ_1:45 ;

hence <*p1,p2,p3*> | (Seg 2) = <*p1,p2*> by A5, A6, FINSEQ_1:44; :: thesis: verum